1 /-
2 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Leonardo de Moura, Mario Carneiro
5 -/
6 import data.list.basic data.pnat.basic data.array.lemmas
src └─────────────┘ └─────────────┘ └───────────────┘
7 logic.basic algebra.group
src └─────────┘ └───────────┘
8 data.list.defs data.nat.basic data.option.basic
src └────────────┘ └────────────┘ └───────────────┘
9 data.bool data.prod
src └───────┘ └───────┘
10 import tactic.finish data.sigma.basic
src └───────────┘ └──────────────┘
11
12 universes u v w
13
14 /-- `bucket_array α β` is the underlying data type for `hash_map α β`,
15 an array of linked lists of key-value pairs. -/
16 def bucket_array (α : Type u) (β : α → Type v) (n : ℕ+) :=
id ┴ └┘
src └┘
typ ┴ └┘
doc └┘
17 array n.1 (list Σ a, β a)
id └───┘ ┴┴ └──┘ ┴ ┴┴ ┴ ┴
src └───┘ ┴ └──┘ ┴ ┴
typ └───┘ ┴┴ └──┘ ┴ ┴┴ ┴ ┴
18
19 /-- Make a hash_map index from a `nat` hash value and a (positive) buffer size -/
20 def hash_map.mk_idx (n : ℕ+) (i : nat) : fin n.1 :=
id └┘ └─┘ └─┘ ┴┴
src └┘ └─┘ └─┘ ┴
typ └┘ └─┘ └─┘ ┴┴
doc └┘
21 ⟨i % n.1, nat.mod_lt _ n.2⟩
id ┴ ┴ ┴┴ └────────┘ ┴┴
src ┴ ┴ └────────┘ ┴
typ ┴ ┴ ┴┴ └────────┘ ┴┴
22
23 namespace bucket_array
24 section
25 parameters {α : Type u} {β : α → Type v} (hash_fn : α → nat)
id └─┘
src └─┘
typ └─┘
26 variables {n : ℕ+} (data : bucket_array α β n)
id └┘ └──────────┘
src └┘ └──────────┘
typ └┘ └──────────┘
doc └┘ └──────────┘
27
28 instance : inhabited (bucket_array α β n) :=
id └───────┘ └──────────┘ ┴ ┴ ┴
src └───────┘ └──────────┘
typ └───────┘ └──────────┘ ┴ ┴ ┴
doc └──────────┘
29 ⟨mk_array _ []⟩
id └──────┘ └┘
src └──────┘ └┘
typ └──────┘ └┘
30
31 /-- Read the bucket corresponding to an element -/
32 def read (a : α) : list Σ a, β a :=
id ┴ └──┘ ┴ ┴┴ ┴ ┴
src └──┘ ┴ ┴
typ ┴ └──┘ ┴ ┴┴ ┴ ┴
33 let bidx := hash_map.mk_idx n (hash_fn a) in
id └──┘ └─────────────┘ ┴ └─────┘ ┴
src └─────────────┘
typ └──┘ └─────────────┘ ┴ └─────┘ ┴
doc └─────────────┘
34 data.read bidx
id └──┘└───┘ └──┘
src └───┘
typ └──┘└───┘ └──┘
35
36 /-- Write the bucket corresponding to an element -/
37 def write (a : α) (l : list Σ a, β a) : bucket_array α β n :=
id ┴ └──┘ ┴ ┴┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
src └──┘ ┴ ┴ └──────────┘
typ ┴ └──┘ ┴ ┴┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘
38 let bidx := hash_map.mk_idx n (hash_fn a) in
id └──┘ └─────────────┘ ┴ └─────┘ ┴
src └─────────────┘
typ └──┘ └─────────────┘ ┴ └─────┘ ┴
doc └─────────────┘
39 data.write bidx l
id └──┘└────┘ └──┘ ┴
src └────┘
typ └──┘└────┘ └──┘ ┴
40
41 /-- Modify (read, apply `f`, and write) the bucket corresponding to an element -/
42 def modify (a : α) (f : list (Σ a, β a) → list (Σ a, β a)) : bucket_array α β n :=
id ┴ └──┘ ┴ ┴┴ ┴ ┴ └──┘ ┴ ┴┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
src └──┘ ┴ ┴ └──┘ ┴ ┴ └──────────┘
typ ┴ └──┘ ┴ ┴┴ ┴ ┴ └──┘ ┴ ┴┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘
43 let bidx := hash_map.mk_idx n (hash_fn a) in
id └──┘ └─────────────┘ ┴ └─────┘ ┴
src └─────────────┘
typ └──┘ └─────────────┘ ┴ └─────┘ ┴
doc └─────────────┘
44 array.write data bidx (f (array.read data bidx))
id └─────────┘ └──┘ └──┘ ┴ └────────┘ └──┘ └──┘
src └─────────┘ └────────┘
typ └─────────┘ └──┘ └──┘ ┴ └────────┘ └──┘ └──┘
45
46 /-- The list of all key-value pairs in the bucket list -/
47 def as_list : list Σ a, β a := data.to_list.join
id └──┘ ┴ ┴┴ ┴ ┴ └──┘└──────┘└───┘
src └──┘ ┴ ┴ └──────┘└───┘
typ └──┘ ┴ ┴┴ ┴ ┴ └──┘└──────┘└───┘
48
49 theorem mem_as_list {a : Σ a, β a} : a ∈ data.as_list ↔ ∃i, a ∈ array.read data i :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ └──┘└──────┘ ┴ ┴┴┴ ┴ ┴ └────────┘ └──┘ ┴
src ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └────────┘
typ ┴ ┴┴ ┴ ┴ ┴ ┴ └──┘└──────┘ ┴ ┴┴┴ ┴ ┴ └────────┘ └──┘ ┴
doc └──────┘
50 have (∃ (l : list (Σ (a : α), β a)) (i : fin (n.val)), a ∈ l ∧ array.read data i = l) ↔
id ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└──┘ ┴ ┴ ┴ ┴ ┴ └────────┘ └──┘ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴ ┴ └─┘ └──┘ ┴ ┴ ┴ └────────┘ ┴ ┴
typ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└──┘ ┴ ┴ ┴ ┴ ┴ └────────┘ └──┘ ┴ ┴ ┴ ┴
51 ∃ (i : fin (n.val)), a ∈ array.read data i,
id ┴ └─┘ ┴└──┘ ┴ ┴ ┴ └────────┘ └──┘ ┴
src ┴ └─┘ └──┘ ┴ ┴ └────────┘
typ ┴ └─┘ ┴└──┘ ┴ ┴ ┴ └────────┘ └──┘ ┴
52 by rw exists_swap; exact exists_congr (λ i, by simp),
id └─────────┘ └──────────┘
src └─┘└─────────┘ └────┘└──────────┘┴ └──┘ ┴└──┘┴
typ └─┘└─────────┘ └────┘└──────────┘┴ └──┘ ┴└──┘┴
doc └─┘ └────┘ ┴ └──┘ ┴└──┘┴
txt └─┘ └────┘ ┴ └──┘ ┴└──┘┴
par └─┘ └────┘ ┴ └──┘ ┴└──┘┴
pid ┴ ┴ ┴ └──┘ └────┘
st └──────────────────────────────────────────┘└───┘┴
53 by simp [as_list]; simpa [array.mem.def, and_comm]
id └─────┘ └───────────┘ └──────┘
src └────┘└─────┘┴ └─────┘└───────────┘└┘└──────┘└─
typ └────┘└─────┘┴ └─────┘└───────────┘└┘└──────┘└─
doc └────┘└─────┘┴ └─────┘ └┘ └─
txt └────┘ ┴ └─────┘ └┘ └─
par └────┘ ┴ └─────┘ └┘ └─
pid ┴┴ ┴ ┴┴ └┘ ┴└
st └────────────────────────────────────────────────
54
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
55 /-- Fold a function `f` over the key-value pairs in the bucket list -/
56 def foldl {δ : Type w} (d : δ) (f : δ → Π a, β a → δ) : δ :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
57 data.foldl d (λ b d, b.foldl (λ r a, f r a.1 a.2) d)
id └──┘└────┘ ┴ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴
src └────┘ └────┘ ┴ ┴
typ └──┘└────┘ ┴ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴
58
59 theorem foldl_eq {δ : Type w} (d : δ) (f : δ → Π a, β a → δ) :
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
60 data.foldl d f = data.as_list.foldl (λ r a, f r a.1 a.2) d :=
id └──┘└────┘ ┴ ┴ ┴ └──┘└──────┘└────┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴
src └────┘ ┴ └──────┘└────┘ ┴ ┴
typ └──┘└────┘ ┴ ┴ ┴ └──┘└──────┘└────┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴
doc └────┘ └──────┘
61 by rw [foldl, as_list, list.foldl_join, ← array.to_list_foldl]
id └───┘ └─────┘ └─────────────┘ └─────────────────┘
src └──┘└───┘└┘└─────┘└┘└─────────────┘└──┘└─────────────────┘└─
typ └──┘└───┘└┘└─────┘└┘└─────────────┘└──┘└─────────────────┘└─
doc └──┘└───┘└┘└─────┘└┘ └──┘ └─
txt └──┘ └┘ └┘ └──┘ └─
par └──┘ └┘ └┘ └──┘ └─
pid └┘ └┘ └┘ └──┘ ┴└
st └────────┘└───────┘└───────────────┘└─────────────────────┘┴└
62
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
63 end
64 end bucket_array
65
66 namespace hash_map
67 section
68 parameters {α : Type u} {β : α → Type v} (hash_fn : α → nat)
id ┴ └──┘ ┴ ┴ └─┘
src └─┘
typ ┴ └──┘ ┴ ┴ └─┘
69
70 /-- Insert the pair `⟨a, b⟩` into the correct location in the bucket array
71 (without checking for duplication) -/
72 def reinsert_aux {n} (data : bucket_array α β n) (a : α) (b : β a) : bucket_array α β n :=
id └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘ └──────────┘
typ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └──────────┘
73 data.modify hash_fn a (λl, ⟨a, b⟩ :: l)
id └──┘└─────┘ └─────┘ ┴ ┴ ┴ ┴ └┘ ┴
src └─────┘ └┘
typ └──┘└─────┘ └─────┘ ┴ ┴ ┴ ┴ └┘ ┴
doc └─────┘
74
75 parameter [decidable_eq α]
id └───────────┘
src └──────────┘
typ └───────────┘
76
77 /-- Search a bucket for a key `a` and return the value -/
78 def find_aux (a : α) : list (Σ a, β a) → option (β a)
id ┴ └──┘ ┴ ┴┴ ┴ ┴ ┴ └────┘ ┴ ┴
src └──┘ ┴ ┴ └────┘
typ ┴ └──┘ ┴ ┴┴ ┴ ┴ ┴ └────┘ ┴ ┴
79 | [] := none
id └┘ └──┘
src └┘ └──┘
typ └┘ └──┘
80 | (⟨a',b⟩::t) := if h : a' = a then some (eq.rec_on h b) else find_aux t
id └┘ ┴ └┘┴ └┘ ┴ ┴ └──┘ └───────┘ ┴ └──────┘
src └┘ └┘ ┴ └──┘ └───────┘ └──────┘
typ └┘ ┴ └┘┴ └┘ ┴ ┴ └──┘ └───────┘ ┴ └──────┘
81
82 theorem find_aux_iff {a : α} {b : β a} : Π {l : list Σ a, β a}, (l.map sigma.fst).nodup → (find_aux a l = some b ↔ sigma.mk a b ∈ l)
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴┴ ┴ ┴ ┴└──┘ └───────┘ └───┘ └──────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ └──┘ └───────┘ └───┘ └──────┘ ┴ └──┘ ┴ └──────┘ ┴
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴┴ ┴ ┴ ┴└──┘ └───────┘ └───┘ └──────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └───┘ └──────┘
83 | [] nd := ⟨λn, by injection n, false.elim⟩
id └┘ ┴ ┴ └────────┘
src └┘ └────────┘ └────────┘
typ └┘ ┴ └────────┘┴ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st └──────────┘
84 | (⟨a',b'⟩::t) nd := begin
id └┘
src └┘
typ └┘
st └─────
85 by_cases a' = a,
id └┘ ┴ ┴
src └───────┘ ┴┴┴
typ └───────┘└┘┴┴┴┴
doc └───────┘ ┴ ┴
txt └───────┘ ┴ ┴
par └───────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────┘└─
86 { clear find_aux_iff, subst h,
id ┴
src └────────────────┘ └────┘
typ └────────────────┘ └────┘┴
doc └────────────────┘ └────┘
txt └────────────────┘ └────┘
par └────────────────┘ └────┘
pid └───────────┘ ┴
st ───┘└────────────────┘└───────┘└─
87 suffices : b' = b ↔ b' = b ∨ sigma.mk a' b ∈ t, {simpa [find_aux, eq_comm]},
id └┘ ┴ └──────┘ └┘ ┴ ┴ ┴ └──────┘ └─────┘
src └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴└──────┘┴ ┴ ┴┴┴ └─────┘└──────┘└┘└─────┘┴
typ └─────────┘ ┴ ┴ ┴ ┴└┘┴ ┴ ┴┴┴└──────┘┴└┘┴┴┴┴┴┴ └─────┘└──────┘└┘└─────┘┴
doc └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘└──────┘└┘ ┴
txt └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └┘ ┴
par └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └┘ ┴
pid └───────┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └┘ ┴
st ─────────────────────────────────────────────────┘└──────────────────────────┘└┘└
88 refine (or_iff_left_of_imp (λ m, _)).symm,
id └────────────────┘
src └─────┘ └────────────────┘┴ └──────────┘
typ └─────┘ └────────────────┘┴ └──────────┘
doc └─────┘ ┴ └──────────┘
txt └─────┘ ┴ └──────────┘
par └─────┘ ┴ └──────────┘
pid ┴ ┴ └─────────┘┴
st ────────────────────────────────────────────┘└─
89 have : a' ∉ t.map sigma.fst, from list.not_mem_of_nodup_cons nd,
id └┘ └───┘ └───────┘ └────────────────────────┘ └┘
src └─────┘ ┴ ┴└───┘┴└───────┘ └───┘└────────────────────────┘┴
typ └─────┘└┘┴ ┴└───┘┴└───────┘ └───┘└────────────────────────┘┴└┘
doc └─────┘ ┴ ┴ ┴ └───┘ ┴
txt └─────┘ ┴ ┴ ┴ └───┘ ┴
par └─────┘ ┴ ┴ ┴ └───┘ ┴
pid └───┘└┘ ┴ ┴ ┴ └───┘ ┴
st ──────────────────────────────┘└──────────────────────────────────┘└─
90 exact this.elim (list.mem_map_of_mem sigma.fst m) },
id └───────┘ └─────────────────┘ └───────┘ ┴
src └────┘└───────┘┴ └─────────────────┘┴└───────┘┴ └┘
typ └────┘└───────┘┴ └─────────────────┘┴└───────┘┴┴└┘
doc └────┘ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴┴
st ─────────────────────────────────────────────────────┘└┘└
91 { have : sigma.mk a b ≠ ⟨a', b'⟩,
id └──────┘ ┴ ┴ ┴ └┘ └┘
src └─────┘└──────┘┴ ┴ ┴┴┴ └┘ ┴
typ └─────┘└──────┘┴┴┴┴┴┴┴ └┘└┘└┘┴
doc └─────┘ ┴ ┴ ┴ ┴ └┘ ┴
txt └─────┘ ┴ ┴ ┴ ┴ └┘ ┴
par └─────┘ ┴ ┴ ┴ ┴ └┘ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ └┘ ┴
st ─────────────────────────────────┘└─
92 { intro e, injection e with e, exact h e.symm },
id ┴ ┴ └────┘
src └─────┘ └────────┘ └─────┘ └────┘ ┴└────┘┴
typ └─────┘ └────────┘┴└─────┘ └────┘┴┴└────┘┴
doc └─────┘ └────────┘ └─────┘ └────┘ ┴ ┴
txt └─────┘ └────────┘ └─────┘ └────┘ ┴ ┴
par └─────┘ └────────┘ └─────┘ └────┘ ┴ ┴
pid └┘ ┴ └─────┘ ┴ ┴ ┴
st ─────┘└─────┘└──────────────────┘└───────────────┘└┘└
93 simp at nd, simp [find_aux, h, ne.symm h, find_aux_iff, nd] }
id └──────┘ ┴ └─────┘ ┴ └┘
src └────────┘ └────┘└──────┘└┘ └┘└─────┘┴ └┘ └┘ └┘
typ └────────┘ └────┘└──────┘└┘┴└┘└─────┘┴┴└┘└──────────┘└┘└┘└┘
doc └────────┘ └────┘└──────┘└┘ └┘ ┴ └┘ └┘ └┘
txt └────────┘ └────┘ └┘ └┘ ┴ └┘ └┘ └┘
par └────────┘ └────┘ └┘ └┘ ┴ └┘ └┘ └┘
pid ┴└───┘ ┴┴ └┘ └┘ ┴ └┘ └┘ ┴┴
st ─────────────┘└────────────────────────────────────────────────┘└─
94 end
st ──┘
95
96 /-- Returns `tt` if the bucket `l` contains the key `a` -/
97 def contains_aux (a : α) (l : list Σ a, β a) : bool :=
id ┴ └──┘ ┴ ┴┴ ┴ ┴ └──┘
src └──┘ ┴ ┴ └──┘
typ ┴ └──┘ ┴ ┴┴ ┴ ┴ └──┘
98 (find_aux a l).is_some
id └──────┘ ┴ ┴ └─────┘
src └──────┘ └─────┘
typ └──────┘ ┴ ┴ └─────┘
doc └──────┘
99
100 theorem contains_aux_iff {a : α} {l : list Σ a, β a} (nd : (l.map sigma.fst).nodup) : contains_aux a l ↔ a ∈ l.map sigma.fst :=
id ┴ └──┘ ┴ ┴┴ ┴ ┴ ┴└──┘ └───────┘ └───┘ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ └───────┘
src └──┘ ┴ ┴ └──┘ └───────┘ └───┘ └──────────┘ ┴ ┴ └──┘ └───────┘
typ ┴ └──┘ ┴ ┴┴ ┴ ┴ ┴└──┘ └───────┘ └───┘ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ └───────┘
doc └───┘ └──────────┘
101 begin
st └─────
102 unfold contains_aux,
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └───────────┘
st ────────────────────┘└─
103 cases h : find_aux a l with b; simp,
id └──────┘ ┴ ┴
src └────┘ └─┘└──────┘┴ ┴ └─────┘ └──┘
typ └────┘ └─┘└──────┘┴┴┴┴└─────┘ └──┘
doc └────┘ └─┘└──────┘┴ ┴ └─────┘ └──┘
txt └────┘ └─┘ ┴ ┴ └─────┘ └──┘
par └────┘ └─┘ ┴ ┴ └─────┘ └──┘
pid ┴ └─┘ ┴ ┴ └─────┘
st ────────────────────────────────────┘└─
104 { assume (b : β a) (m : sigma.mk a b ∈ l),
id ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src └──────────┘ ┴ └─────┘└──────┘┴ ┴ ┴┴┴ ┴
typ └──────────┘┴┴┴└─────┘└──────┘┴┴┴┴┴┴┴┴┴
doc └──────────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
txt └──────────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
par └──────────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
pid └──────────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
st ───┘└─────────────────────────────────────┘└─
105 rw (find_aux_iff nd).2 m at h,
id └──────────┘ └┘ ┴
src └─┘ └──────────┘┴ └──┘ └───┘
typ └─┘ └──────────┘┴└┘└──┘┴└───┘
doc └─┘ ┴ └──┘ └───┘
txt └─┘ ┴ └──┘ └───┘
par └─┘ ┴ └──┘ └───┘
pid ┴ ┴ └──┘ └───┘
st ────────────────────────────────┘└─
106 contradiction },
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ─────────────────┘└┘└
107 { show ∃ (b : β a), sigma.mk a b ∈ l,
id ┴ ┴ ┴ └──────┘ ┴ ┴
src └───┘┴└────┘ ┴ ┴┴┴└──────┘┴ ┴ ┴ ┴
typ └───┘┴└────┘┴┴ ┴┴┴└──────┘┴┴┴ ┴ ┴┴
doc └───┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └───┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └───┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────
108 exact ⟨_, (find_aux_iff nd).1 h⟩ },
id └──────────┘ └┘ ┴
src └────┘ └─┘ └──────────┘┴ └──┘ └┘
typ └────┘ └─┘ └──────────┘┴└┘└──┘┴└┘
doc └────┘ └─┘ ┴ └──┘ └┘
txt └────┘ └─┘ ┴ └──┘ └┘
par └────┘ └─┘ ┴ └──┘ └┘
pid ┴ └─┘ ┴ └──┘ ┴┴
st ────────────────────────────────────┘└──
109 end
st ──┘
110
111 /-- Modify a bucket to replace a value in the list. Leaves the list
112 unchanged if the key is not found. -/
113 def replace_aux (a : α) (b : β a) : list (Σ a, β a) → list (Σ a, β a)
id ┴ ┴ ┴ └──┘ ┴ ┴┴ ┴ ┴ ┴ └──┘ ┴ ┴┴ ┴ ┴
src └──┘ ┴ ┴ └──┘ ┴ ┴
typ ┴ ┴ ┴ └──┘ ┴ ┴┴ ┴ ┴ ┴ └──┘ ┴ ┴┴ ┴ ┴
114 | [] := []
id └┘ └┘
src └┘ └┘
typ └┘ └┘
115 | (⟨a', b'⟩::t) := if a' = a then ⟨a, b⟩::t else ⟨a', b'⟩ :: replace_aux t
id └┘ └┘ └┘┴ ┴ ┴ ┴ ┴ └┘ └┘ └─────────┘
src └┘ ┴ └┘ └┘
typ └┘ └┘ └┘┴ ┴ ┴ ┴ ┴ └┘ └┘ └─────────┘
116
117 /-- Modify a bucket to remove a key, if it exists. -/
118 def erase_aux (a : α) : list (Σ a, β a) → list (Σ a, β a)
id ┴ └──┘ ┴ ┴┴ ┴ ┴ ┴ └──┘ ┴ ┴┴ ┴ ┴
src └──┘ ┴ ┴ └──┘ ┴ ┴
typ ┴ └──┘ ┴ ┴┴ ┴ ┴ ┴ └──┘ ┴ ┴┴ ┴ ┴
119 | [] := []
id └┘ └┘
src └┘ └┘
typ └┘ └┘
120 | (⟨a', b'⟩::t) := if a' = a then t else ⟨a', b'⟩ :: erase_aux t
id └┘ └┘ └┘┴ ┴ ┴ └┘ └───────┘
src └┘ ┴ └┘
typ └┘ └┘ └┘┴ ┴ ┴ └┘ └───────┘
121
122 /-- The predicate `valid bkts sz` means that `bkts` satisfies the `hash_map`
123 invariants: There are exactly `sz` elements in it, every pair is in the
124 bucket determined by its key and the hash function, and no key appears
125 multiple times in the list. -/
126 structure valid {n} (bkts : bucket_array α β n) (sz : nat) : Prop :=
id ┴ └──────────┘ ┴ ┴ ┴ └─┘
src └──────────┘ └─┘
typ ┴ └──────────┘ ┴ ┴ ┴ └─┘
doc └──────────┘
127 (len : bkts.as_list.length = sz)
id └──┘└──────┘└─────┘ ┴ └┘
src └──────┘└─────┘ ┴
typ └──┘└──────┘└─────┘ ┴ └┘
doc └──────┘
128 (idx : ∀ {i} {a : Σ a, β a}, a ∈ array.read bkts i →
id ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └────────┘ └──┘ ┴
src ┴ ┴ ┴ └────────┘
typ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └────────┘ └──┘ ┴
129 mk_idx n (hash_fn a.1) = i)
id └────┘ ┴ └─────┘ ┴┴ ┴ ┴
src └────┘ ┴ ┴
typ └────┘ ┴ └─────┘ ┴┴ ┴ ┴
doc └────┘
130 (nodup : ∀i, ((array.read bkts i).map sigma.fst).nodup)
id ┴ └────────┘ └──┘ ┴ └─┘ └───────┘ └───┘
src └────────┘ └─┘ └───────┘ └───┘
typ ┴ └────────┘ └──┘ ┴ └─┘ └───────┘ └───┘
doc └───┘
131
132 theorem valid.idx_enum {n} {bkts : bucket_array α β n} {sz : nat} (v : valid bkts sz)
id └──────────┘ ┴ ┴ ┴ └─┘ └───┘ └──┘ └┘
src └──────────┘ └─┘ └───┘
typ └──────────┘ ┴ ┴ ┴ └─┘ └───┘ └──┘ └┘
doc └──────────┘ └───┘
133 {i l} (he : (i, l) ∈ bkts.to_list.enum) {a} {b : β a} (hl : sigma.mk a b ∈ l) :
id ┴┴ ┴ ┴ └──┘└──────┘└───┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src ┴ ┴ └──────┘└───┘ └──────┘ ┴
typ ┴┴ ┴ ┴ └──┘└──────┘└───┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
134 ∃ h, mk_idx n (hash_fn a) = ⟨i, h⟩ :=
id ┴ ┴┴ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴
src ┴ ┴ └────┘ ┴
typ ┴ ┴┴ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └────┘
135 (array.mem_to_list_enum.mp he).imp (λ h e, by subst e; exact v.idx hl)
id └────────────────────┘└─┘ └┘ └─┘ ┴ ┴ ┴ └───┘ └┘
src └────────────────────┘└─┘ └─┘ └────┘ └────┘└───┘┴
typ └────────────────────┘└─┘ └┘ └─┘ ┴ ┴ └────┘┴ └────┘└───┘┴└┘
doc └────┘ └────┘ ┴
txt └────┘ └────┘ ┴
par └────┘ └────┘ ┴
pid ┴ ┴ ┴
st └──────────────────────┘
136
137 theorem valid.idx_enum_1 {n} {bkts : bucket_array α β n} {sz : nat} (v : valid bkts sz)
id └──────────┘ ┴ ┴ ┴ └─┘ └───┘ └──┘ └┘
src └──────────┘ └─┘ └───┘
typ └──────────┘ ┴ ┴ ┴ └─┘ └───┘ └──┘ └┘
doc └──────────┘ └───┘
138 {i l} (he : (i, l) ∈ bkts.to_list.enum) {a} {b : β a} (hl : sigma.mk a b ∈ l) :
id ┴┴ ┴ ┴ └──┘└──────┘└───┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src ┴ ┴ └──────┘└───┘ └──────┘ ┴
typ ┴┴ ┴ ┴ └──┘└──────┘└───┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
139 (mk_idx n (hash_fn a)).1 = i :=
id └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴
src └────┘ ┴ ┴
typ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └────┘
140 let ⟨h, e⟩ := v.idx_enum _ he hl in by rw e; refl
id └─┘ ┴└───────┘ └┘ └┘ ┴
src └───────┘ └─┘ └────
typ └─┘ ┴└───────┘ └┘ └┘ └─┘┴ └────
doc └─┘ └────
txt └─┘ └────
par └─┘ └────
pid ┴ └
st └───────────
141
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
142 theorem valid.as_list_nodup {n} {bkts : bucket_array α β n} {sz : nat} (v : valid bkts sz) : (bkts.as_list.map sigma.fst).nodup :=
id └──────────┘ ┴ ┴ ┴ └─┘ └───┘ └──┘ └┘ └──┘└──────┘└──┘ └───────┘ └───┘
src └──────────┘ └─┘ └───┘ └──────┘└──┘ └───────┘ └───┘
typ └──────────┘ ┴ ┴ ┴ └─┘ └───┘ └──┘ └┘ └──┘└──────┘└──┘ └───────┘ └───┘
doc └──────────┘ └───┘ └──────┘ └───┘
143 begin
st └─────
144 suffices : (bkts.to_list.map (list.map sigma.fst)).pairwise list.disjoint,
id └──────────────┘ └──────┘ └───────┘ └───────────┘
src └─────────┘ └──────────────┘┴ └──────┘┴└───────┘└──────────┘└───────────┘
typ └─────────┘ └──────────────┘┴ └──────┘┴└───────┘└──────────┘└───────────┘
doc └─────────┘ ┴ ┴ └──────────┘└───────────┘
txt └─────────┘ ┴ ┴ └──────────┘
par └─────────┘ ┴ ┴ └──────────┘
pid └───────┘└┘ ┴ ┴ └──────────┘
st ──────────────────────────────────────────────────────────────────────────┘└─
145 { simp [bucket_array.as_list, list.nodup_join, this],
id └──────────────────┘ └─────────────┘ └──┘
src └────┘└──────────────────┘└┘└─────────────┘└┘ ┴
typ └────┘└──────────────────┘└┘└─────────────┘└┘└──┘┴
doc └────┘└──────────────────┘└┘ └┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st ───┘└────────────────────────────────────────────────┘└─
146 change ∀ l s, array.mem s bkts → list.map sigma.fst s = l → l.nodup,
id └───────┘ └──┘ └──────┘ └───────┘ ┴ └────┘
src └─────┘ └──┘ ┴└───────┘┴ ┴ ┴ ┴└──────┘┴└───────┘┴ ┴┴┴ ┴ ┴ └────┘
typ └─────┘ └──┘ ┴└───────┘┴ ┴└──┘┴ ┴└──────┘┴└───────┘┴ ┴┴┴ ┴ ┴ └────┘
doc └─────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘
txt └─────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────┘└─
147 introv m e, subst e, cases m with i e, subst e,
id ┴ ┴ ┴
src └────────┘ └────┘ └────┘ └───────┘ └────┘
typ └────────┘ └────┘┴ └────┘┴└───────┘ └────┘┴
doc └────────┘ └────┘ └────┘ └───────┘ └────┘
txt └────────┘ └────┘ └────┘ └───────┘ └────┘
par └────────┘ └────┘ └────┘ └───────┘ └────┘
pid └──┘ ┴ ┴ └───────┘ ┴
st ─────────────┘└───────┘└────────────────┘└───────┘└─
148 apply v.nodup },
src └────┘ ┴
typ └────┘ ┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────┘└┘└
149 rw [← list.enum_map_snd bkts.to_list, list.pairwise_map, list.pairwise_map],
id └───────────────┘ └──────────┘ └───────────────┘ └───────────────┘
src └────┘└───────────────┘┴└──────────┘└┘└───────────────┘└┘└───────────────┘┴
typ └────┘└───────────────┘┴└──────────┘└┘└───────────────┘└┘└───────────────┘┴
doc └────┘ ┴ └┘ └┘ ┴
txt └────┘ ┴ └┘ └┘ ┴
par └────┘ ┴ └┘ └┘ ┴
pid └──┘ ┴ └┘ └┘ ┴
st ─────────────────────────────────────┘└─────────────────┘└─────────────────┘└──
150 have : (bkts.to_list.enum.map prod.fst).nodup := by simp [list.nodup_range],
id └───────────────────┘ └──────┘ └──────────────┘
src └─────┘ └───────────────────┘┴└──────┘└─────────┘ ┴└────┘└──────────────┘┴
typ └─────┘ └───────────────────┘┴└──────┘└─────────┘ ┴└────┘└──────────────┘┴
doc └─────┘ ┴ └─────────┘ ┴└────┘ ┴
txt └─────┘ ┴ └─────────┘ ┴└────┘ ┴
par └─────┘ ┴ └─────────┘ ┴└────┘ ┴
pid └───┘└┘ ┴ └────┘└───┘ └─────┘ ┴
st ────────────────────────────────────────────────────┘└──────────────────────┘└─
151 refine list.pairwise.imp_of_mem _ ((list.pairwise_map _).1 this),
id └──────────────────────┘ └───────────────┘ └──┘
src └─────┘└──────────────────────┘└─┘ └───────────────┘└────┘ ┴
typ └─────┘└──────────────────────┘└─┘ └───────────────┘└────┘└──┘┴
doc └─────┘ └─┘ └────┘ ┴
txt └─────┘ └─┘ └────┘ ┴
par └─────┘ └─┘ └────┘ ┴
pid ┴ └─┘ └────┘ ┴
st ─────────────────────────────────────────────────────────────────┘└─
152 rw prod.forall, intros i l₁,
id └─────────┘
src └─┘└─────────┘ └─────────┘
typ └─┘└─────────┘ └─────────┘
doc └─┘ └─────────┘
txt └─┘ └─────────┘
par └─┘ └─────────┘
pid ┴ └───┘
st ───────────────┘└───────────┘└─
153 rw prod.forall, intros j l₂ me₁ me₂ ij,
id └─────────┘
src └─┘└─────────┘ └────────────────────┘
typ └─┘└─────────┘ └────────────────────┘
doc └─┘ └────────────────────┘
txt └─┘ └────────────────────┘
par └─┘ └────────────────────┘
pid ┴ └──────────────┘
st ───────────────┘└──────────────────────┘└─
154 simp [list.disjoint], intros a b ml₁ b' ml₂,
id └───────────┘
src └────┘└───────────┘┴ └───────────────────┘
typ └────┘└───────────┘┴ └───────────────────┘
doc └────┘└───────────┘┴ └───────────────────┘
txt └────┘ ┴ └───────────────────┘
par └────┘ ┴ └───────────────────┘
pid ┴┴ ┴ └─────────────┘
st ─────────────────────┘└─────────────────────┘└─
155 apply ij, rwa [← v.idx_enum_1 _ me₁ ml₁, ← v.idx_enum_1 _ me₂ ml₂]
id └──────────┘ └─┘ └─┘ └──────────┘ └─┘ └─┘
src └────┘ └─────┘└──────────┘└─┘ ┴ └──┘└──────────┘└─┘ ┴ └┘
typ └────┘ └─────┘└──────────┘└─┘└─┘┴└─┘└──┘└──────────┘└─┘└─┘┴└─┘└┘
doc └────┘ └─────┘ └─┘ ┴ └──┘ └─┘ ┴ └┘
txt └────┘ └─────┘ └─┘ ┴ └──┘ └─┘ ┴ └┘
par └────┘ └─────┘ └─┘ ┴ └──┘ └─┘ ┴ └┘
pid ┴ └──┘ └─┘ ┴ └──┘ └─┘ ┴ ┴┴
st ─────────┘└─────────────────────────────┘└────────────────────────┘┴┴
156 end
st └─┘
157
158 theorem mk_as_list (n : ℕ+) : bucket_array.as_list (mk_array n.1 [] : bucket_array α β n) = [] :=
id └┘ └──────────────────┘ └──────┘ ┴┴ └┘ └──────────┘ ┴ ┴ ┴ ┴ └┘
src └┘ └──────────────────┘ └──────┘ ┴ └┘ └──────────┘ ┴ └┘
typ └┘ └──────────────────┘ └──────┘ ┴┴ └┘ └──────────┘ ┴ ┴ ┴ ┴ └┘
doc └┘ └──────────────────┘ └──────────┘
159 list.eq_nil_iff_forall_not_mem.mpr $ λ x m,
id └────────────────────────────┘└──┘ ┴ ┴
src └────────────────────────────┘└──┘
typ └────────────────────────────┘└──┘ ┴ ┴
160 let ⟨i, h⟩ := (bucket_array.mem_as_list _).1 m in h
id └─┘ ┴ └──────────────────────┘ ┴ ┴
src └──────────────────────┘ ┴
typ └─┘ ┴ └──────────────────────┘ ┴ ┴
161
162 theorem mk_valid (n : ℕ+) : @valid n (mk_array n.1 []) 0 :=
id └┘ └───┘ ┴ └──────┘ ┴┴ └┘
src └┘ └───┘ └──────┘ ┴ └┘
typ └┘ └───┘ ┴ └──────┘ ┴┴ └┘
doc └┘ └───┘
163 ⟨by simp [mk_as_list], λ i a h, by cases h, λ i, list.nodup_nil⟩
id └────────┘ ┴ ┴ ┴ ┴ ┴ └────────────┘
src └────┘└────────┘┴ └────┘ └────────────┘
typ └────┘└────────┘┴ ┴ ┴ ┴ └────┘┴ ┴ └────────────┘
doc └────┘ ┴ └────┘
txt └────┘ ┴ └────┘
par └────┘ ┴ └────┘
pid ┴┴ ┴ ┴
st └────────────────┘ └──────┘
164
165 theorem valid.find_aux_iff {n} {bkts : bucket_array α β n} {sz : nat} (v : valid bkts sz) {a : α} {b : β a} :
id └──────────┘ ┴ ┴ ┴ └─┘ └───┘ └──┘ └┘ ┴ ┴ ┴
src └──────────┘ └─┘ └───┘
typ └──────────┘ ┴ ┴ ┴ └─┘ └───┘ └──┘ └┘ ┴ ┴ ┴
doc └──────────┘ └───┘
166 find_aux a (bkts.read hash_fn a) = some b ↔ sigma.mk a b ∈ bkts.as_list :=
id └──────┘ ┴ └──┘└───┘ └─────┘ ┴ ┴ └──┘ ┴ ┴ └──────┘ ┴ ┴ ┴ └──┘└──────┘
src └──────┘ └───┘ ┴ └──┘ ┴ └──────┘ ┴ └──────┘
typ └──────┘ ┴ └──┘└───┘ └─────┘ ┴ ┴ └──┘ ┴ ┴ └──────┘ ┴ ┴ ┴ └──┘└──────┘
doc └──────┘ └───┘ └──────┘
167 (find_aux_iff (v.nodup _)).trans $
id └──────────┘ ┴└────┘ └───┘
src └──────────┘ └────┘ └───┘
typ └──────────┘ ┴└────┘ └───┘
168 by rw bkts.mem_as_list; exact ⟨λ h, ⟨_, h⟩, λ ⟨i, h⟩, (v.idx h).symm ▸ h⟩
id ┴ └───┘ ┴
src └─┘ └────┘ └──┘ └─┘ └─┘ └┘ └┘ └─┘ └───┘┴ └─────┘┴┴ └─
typ └─┘└──────────────┘ └────┘ └──┘ └─┘ └─┘ └┘ └┘┴└─┘ └───┘┴ └─────┘┴┴ └─
doc └─┘ └────┘ └──┘ └─┘ └─┘ └┘ └┘ └─┘ ┴ └─────┘ ┴ └─
txt └─┘ └────┘ └──┘ └─┘ └─┘ └┘ └┘ └─┘ ┴ └─────┘ ┴ └─
par └─┘ └────┘ └──┘ └─┘ └─┘ └┘ └┘ └─┘ ┴ └─────┘ ┴ └─
pid ┴ ┴ └──┘ └─┘ └─┘ └┘ └┘ └─┘ ┴ └─────┘ ┴ ┴└
st └───────────────────────────────────────────────────────────────────────
169
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
170 theorem valid.contains_aux_iff {n} {bkts : bucket_array α β n} {sz : nat} (v : valid bkts sz) (a : α) :
id └──────────┘ ┴ ┴ ┴ └─┘ └───┘ └──┘ └┘ ┴
src └──────────┘ └─┘ └───┘
typ └──────────┘ ┴ ┴ ┴ └─┘ └───┘ └──┘ └┘ ┴
doc └──────────┘ └───┘
171 contains_aux a (bkts.read hash_fn a) ↔ a ∈ bkts.as_list.map sigma.fst :=
id └──────────┘ ┴ └──┘└───┘ └─────┘ ┴ ┴ ┴ ┴ └──┘└──────┘└──┘ └───────┘
src └──────────┘ └───┘ ┴ ┴ └──────┘└──┘ └───────┘
typ └──────────┘ ┴ └──┘└───┘ └─────┘ ┴ ┴ ┴ ┴ └──┘└──────┘└──┘ └───────┘
doc └──────────┘ └───┘ └──────┘
172 by simp [contains_aux, option.is_some_iff_exists, v.find_aux_iff hash_fn]
id └──────────┘ └───────────────────────┘ └────────────┘ └─────┘
src └────┘└──────────┘└┘└───────────────────────┘└┘└────────────┘┴ └─
typ └────┘└──────────┘└┘└───────────────────────┘└┘└────────────┘┴└─────┘└─
doc └────┘└──────────┘└┘ └┘ ┴ └─
txt └────┘ └┘ └┘ ┴ └─
par └────┘ └┘ └┘ ┴ └─
pid ┴┴ └┘ └┘ ┴ ┴└
st └───────────────────────────────────────────────────────────────────────
173
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
174 section
175 parameters {n : ℕ+} {bkts : bucket_array α β n}
id └┘ └──────────┘
src └┘ └──────────┘
typ └┘ └──────────┘
doc └┘ └──────────┘
176 {bidx : fin n.1} {f : list (Σ a, β a) → list (Σ a, β a)}
id └─┘ ┴ └──┘ ┴ ┴┴ ┴ └──┘ ┴ ┴┴ ┴
src └─┘ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴
typ └─┘ ┴ └──┘ ┴ ┴┴ ┴ └──┘ ┴ ┴┴ ┴
177 (u v1 v2 w : list Σ a, β a)
id └──┘ ┴ ┴┴ ┴
src └──┘ ┴ ┴
typ └──┘ ┴ ┴┴ ┴
178
179 local notation `L` := array.read bkts bidx
id └────────┘
src └────────┘
typ └────────┘
180 private def bkts' : bucket_array α β n := array.write bkts bidx (f L)
id └──────────┘ ┴ ┴ ┴ └─────────┘ └──┘ └──┘ ┴ ┴
src └──────────┘ └─────────┘ ┴
typ └──────────┘ ┴ ┴ ┴ └─────────┘ └──┘ └──┘ ┴ ┴
doc └──────────┘
181
182 variables (hl : L = u ++ v1 ++ w)
id ┴ ┴ └┘ └┘
src ┴ ┴ └┘ └┘
typ ┴ ┴ └┘ └┘
183 (hfl : f L = u ++ v2 ++ w)
id ┴ ┴ └┘ └┘
src ┴ ┴ └┘ └┘
typ ┴ ┴ └┘ └┘
184 include hl hfl
185
186 theorem append_of_modify : ∃ u' w', bkts.as_list = u' ++ v1 ++ w' ∧ bkts'.as_list = u' ++ v2 ++ w' :=
id ┴ └┘ └┘┴ └──┘└──────┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴ └───┘└──────┘ ┴ └┘ └┘ └┘ └┘ └┘
src ┴ ┴ └──────┘ ┴ └┘ └┘ ┴ └───┘└──────┘ ┴ └┘ └┘
typ ┴ └┘ └┘┴ └──┘└──────┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴ └───┘└──────┘ ┴ └┘ └┘ └┘ └┘ └┘
doc └──────┘ └──────┘
187 begin
st └─────
188 unfold bucket_array.as_list,
src └─────────────────────────┘
typ └─────────────────────────┘
doc └─────────────────────────┘
txt └─────────────────────────┘
par └─────────────────────────┘
pid └───────────────────┘
st ──────────────────────────────┘└─
189 have h : bidx.1 < bkts.to_list.length, {simp [bidx.2]},
id └──┘ ┴ └─────────────────┘ └──┘
src └───────┘ └─┘┴┴└─────────────────┘ └────┘ └─┘
typ └───────┘└──┘└─┘┴┴└─────────────────┘ └────┘└──┘└─┘
doc └───────┘ └─┘ ┴ └────┘ └─┘
txt └───────┘ └─┘ ┴ └────┘ └─┘
par └───────┘ └─┘ ┴ └────┘ └─┘
pid └────┘└─┘ └─┘ ┴ ┴┴ └─┘
st ────────────────────────────────────────┘└──────────────┘└┘└
190 refine ⟨(bkts.to_list.take bidx.1).join ++ u, w ++ (bkts.to_list.drop (bidx.1+1)).join, _, _⟩,
id └───────────────┘ └┘ ┴ ┴ └───────────────┘ └──┘ ┴
src └─────┘ └───────────────┘┴ └───────┘└┘┴ └┘ ┴ ┴ └───────────────┘┴ └┘┴└─────────────┘
typ └─────┘ └───────────────┘┴ └───────┘└┘┴┴└┘┴┴ ┴ └───────────────┘┴ └──┘└┘┴└─────────────┘
doc └─────┘ ┴ └───────┘ ┴ └┘ ┴ ┴ ┴ └┘ └─────────────┘
txt └─────┘ ┴ └───────┘ ┴ └┘ ┴ ┴ ┴ └┘ └─────────────┘
par └─────┘ ┴ └───────┘ ┴ └┘ ┴ ┴ ┴ └┘ └─────────────┘
pid ┴ ┴ └───────┘ ┴ └┘ ┴ ┴ ┴ └┘ └─────────────┘
st ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
191 { conv { to_lhs,
src └─────┘└────┘└─
typ └─────┘└────┘└─
txt └─────┘└────┘└─
par └─────┘└────┘└─
pid ┴└─────────
st ─────┘└────┘└─────┘└─
192 rw [← list.take_append_drop bidx.1 bkts.to_list, list.drop_eq_nth_le_cons h],
id └───────────────────┘ └──┘ └──────────┘ └──────────────────────┘ ┴
src ───────┘└────┘└───────────────────┘┴ └─┘└──────────┘└┘└──────────────────────┘┴ ┴└─
typ ───────┘└────┘└───────────────────┘┴└──┘└─┘└──────────┘└┘└──────────────────────┘┴┴┴└─
txt ───────┘└────┘ ┴ └─┘ └┘ ┴ ┴└─
par ───────┘└────┘ ┴ └─┘ └┘ ┴ ┴└─
pid ─────────────┘ ┴ └─┘ └┘ ┴ └──
st ──────────────────────────────────────────────────────┘└──────────────────────────┘ └─
193 simp [hl] }, simp },
id └┘
src ───────┘└────┘ └┘┴ └───┘
typ ───────┘└────┘└┘└┘┴ └───┘
doc └───┘
txt ───────┘└────┘ └┘┴ └───┘
par ───────┘└────┘ └┘┴ └───┘
pid ─────────────┘ └─┘ ┴
st ─────────────────┘└┘└────┘└┘└
194 { conv { to_lhs,
src └─────┘└────┘└─
typ └─────┘└────┘└─
txt └─────┘└────┘└─
par └─────┘└────┘└─
pid ┴└─────────
st ───────────┘└─────┘└─
195 rw [bkts', array.write_to_list, list.update_nth_eq_take_cons_drop _ h],
id └───┘ └─────────────────┘ └───────────────────────────────┘ ┴
src ───────┘└──┘└───┘└┘└─────────────────┘└┘└───────────────────────────────┘└─┘ ┴└─
typ ───────┘└──┘└───┘└┘└─────────────────┘└┘└───────────────────────────────┘└─┘┴┴└─
txt ───────┘└──┘ └┘ └┘ └─┘ ┴└─
par ───────┘└──┘ └┘ └┘ └─┘ ┴└─
pid ───────────┘ └┘ └┘ └─┘ └──
st ────────────────┘└───────────────────┘└─────────────────────────────────────┘ └─
196 simp [hfl] }, simp }
id └─┘
src ───────┘└────┘ └┘┴ └───┘
typ ───────┘└────┘└─┘└┘┴ └───┘
doc └───┘
txt ───────┘└────┘ └┘┴ └───┘
par ───────┘└────┘ └┘┴ └───┘
pid ─────────────┘ └─┘ ┴
st ──────────────────┘└┘└────┘└─
197 end
st ────┘
198
199 variables (hvnd : (v2.map sigma.fst).nodup)
id └──┘ └───────┘ └───┘
src └──┘ └───────┘ └───┘
typ └──┘ └───────┘ └───┘
doc └───┘
200 (hal : ∀ (a : Σ a, β a), a ∈ v2 → mk_idx n (hash_fn a.1) = bidx)
id ┴ ┴┴ ┴ ┴ ┴ └────┘ ┴┴ ┴
src ┴ ┴ ┴ └────┘ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ └────┘ ┴┴ ┴
doc └────┘
201 (djuv : (u.map sigma.fst).disjoint (v2.map sigma.fst))
id └──┘ └───────┘ └──────┘ └──┘ └───────┘
src └──┘ └───────┘ └──────┘ └──┘ └───────┘
typ └──┘ └───────┘ └──────┘ └──┘ └───────┘
doc └──────┘
202 (djwv : (w.map sigma.fst).disjoint (v2.map sigma.fst))
id └──┘ └───────┘ └──────┘ └──┘ └───────┘
src └──┘ └───────┘ └──────┘ └──┘ └───────┘
typ └──┘ └───────┘ └──────┘ └──┘ └───────┘
doc └──────┘
203 include hvnd hal djuv djwv
204
205 theorem valid.modify {sz : ℕ} (v : valid bkts sz) : sz + v2.length ≥ v1.length ∧ valid bkts' (sz + v2.length - v1.length) :=
id ┴ └───┘ └──┘ └┘ └┘ ┴ └┘└─────┘ ┴ └┘└─────┘ ┴ └───┘ └───┘ └┘ ┴ └┘└─────┘ ┴ └┘└─────┘
src ┴ └───┘ ┴ └─────┘ ┴ └─────┘ ┴ └───┘ └───┘ ┴ └─────┘ ┴ └─────┘
typ ┴ └───┘ └──┘ └┘ └┘ ┴ └┘└─────┘ ┴ └┘└─────┘ ┴ └───┘ └───┘ └┘ ┴ └┘└─────┘ ┴ └┘└─────┘
doc └───┘ └───┘
206 begin
st └─────
207 rcases append_of_modify u v1 v2 w hl hfl with ⟨u', w', e₁, e₂⟩,
id └──────────────┘ ┴ └┘ └┘ ┴ └┘ └─┘
src └─────┘└──────────────┘┴ ┴ ┴ ┴ ┴ ┴ └────────────────────┘
typ └─────┘└──────────────┘┴┴┴└┘┴└┘┴┴┴└┘┴└─┘└────────────────────┘
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────────┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────────┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────────┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────────┘
st ─────────────────────────────────────────────────────────────────┘└─
208 rw [← v.len, e₁],
id └┘
src └────┘ └┘ ┴
typ └────┘└───┘└┘└┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid └──┘ └┘ ┴
st ──────────────┘└──┘└──
209 suffices : valid bkts' (u' ++ v2 ++ w').length,
id └───┘ └┘ └┘ └┘ └┘
src └─────────┘ ┴└───┘┴ ┴└┘┴ ┴ ┴ └──────┘
typ └─────────┘ ┴└───┘┴ └┘┴└┘┴└┘┴ ┴└┘└──────┘
doc └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
txt └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
par └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
pid └───────┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘┴
st ─────────────────────────────────────────────────┘└─
210 { simpa [ge, nat.le_add_right, nat.add_sub_cancel_left] },
id └┘ └──────────────┘ └─────────────────────┘
src └─────┘└┘└┘└──────────────┘└┘└─────────────────────┘└┘
typ └─────┘└┘└┘└──────────────┘└┘└─────────────────────┘└┘
doc └─────┘ └┘ └┘ └┘
txt └─────┘ └┘ └┘ └┘
par └─────┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ ┴┴
st ─────┘└────────────────────────────────────────────────────┘└┘└
211 refine ⟨congr_arg _ e₂, λ i a, _, λ i, _⟩,
id └───────┘ └┘
src └─────┘ └───────┘└─┘ └┘ └───────┘ └────┘
typ └─────┘ └───────┘└─┘└┘└┘ └───────┘ └────┘
doc └─────┘ └─┘ └┘ └───────┘ └────┘
txt └─────┘ └─┘ └┘ └───────┘ └────┘
par └─────┘ └─┘ └┘ └───────┘ └────┘
pid ┴ └─┘ └┘ └───────┘ └────┘
st ────────────────────────────────────────────┘└─
212 { by_cases bidx = i,
id └──┘ ┴ ┴
src └───────┘ ┴┴┴
typ └───────┘└──┘┴┴┴┴
doc └───────┘ ┴ ┴
txt └───────┘ ┴ ┴
par └───────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────┘└───────────────┘└─
213 { subst i, rw [bkts', array.read_write, hfl],
id ┴ └───┘ └──────────────┘ └─┘
src └────┘ └──┘└───┘└┘└──────────────┘└┘ ┴
typ └────┘┴ └──┘└───┘└┘└──────────────┘└┘└─┘┴
doc └────┘ └──┘ └┘ └┘ ┴
txt └────┘ └──┘ └┘ └┘ ┴
par └────┘ └──┘ └┘ └┘ ┴
pid ┴ └┘ └┘ └┘ ┴
st ───────┘└─────┘└─────────┘└────────────────┘└───┘└──
214 have := @valid.idx _ _ _ v bidx a,
id ┴ └──┘ ┴
src └──────┘ └─────┘ ┴ ┴
typ └──────┘ └─────┘┴┴└──┘┴┴
doc └──────┘ └─────┘ ┴ ┴
txt └──────┘ └─────┘ ┴ ┴
par └──────┘ └─────┘ ┴ ┴
pid └───┘└─┘ └─────┘ ┴ ┴
st ────────────────────────────────────────┘└─
215 simp only [hl, list.mem_append, or_imp_distrib, forall_and_distrib] at this ⊢,
id └┘ └─────────────┘ └────────────┘ └────────────────┘
src └─────────┘ └┘└─────────────┘└┘└────────────┘└┘└────────────────┘└─────────┘
typ └─────────┘└┘└┘└─────────────┘└┘└────────────┘└┘└────────────────┘└─────────┘
doc └─────────┘ └┘ └┘ └┘ └─────────┘
txt └─────────┘ └┘ └┘ └┘ └─────────┘
par └─────────┘ └┘ └┘ └┘ └─────────┘
pid ┴└──┘└┘ └┘ └┘ └┘ ┴┴└───────┘
st ────────────────────────────────────────────────────────────────────────────────────┘└─
216 exact ⟨⟨this.1.1, hal _⟩, this.2⟩ },
id └─┘ └──┘
src └────┘ └────┘ └───┘ └──┘
typ └────┘ └────┘└─┘└───┘└──┘└──┘
doc └────┘ └────┘ └───┘ └──┘
txt └────┘ └────┘ └───┘ └──┘
par └────┘ └────┘ └───┘ └──┘
pid ┴ └────┘ └───┘ └─┘┴
st ─────────────────────────────────────────┘└┘└
217 { rw [bkts', array.read_write_of_ne _ _ h], apply v.idx } },
id └───┘ └────────────────────┘ ┴
src └──┘└───┘└┘└────────────────────┘└───┘ ┴ └────┘ ┴
typ └──┘└───┘└┘└────────────────────┘└───┘┴┴ └────┘ ┴
doc └──┘ └┘ └───┘ ┴ └────┘ ┴
txt └──┘ └┘ └───┘ ┴ └────┘ ┴
par └──┘ └┘ └───┘ ┴ └────┘ ┴
pid └┘ └┘ └───┘ ┴ ┴ ┴
st ────────────────┘└────────────────────────────┘└─────────────┘└──┘└
218 { by_cases bidx = i,
id └──┘ ┴
src └───────┘ ┴ ┴
typ └───────┘└──┘┴ ┴┴
doc └───────┘ ┴ ┴
txt └───────┘ ┴ ┴
par └───────┘ ┴ ┴
pid ┴ ┴ ┴
st ──────────────────────┘└─
219 { subst i, rw [bkts', array.read_write, hfl],
id ┴ └───┘ └──────────────┘ └─┘
src └────┘ └──┘└───┘└┘└──────────────┘└┘ ┴
typ └────┘┴ └──┘└───┘└┘└──────────────┘└┘└─┘┴
doc └────┘ └──┘ └┘ └┘ ┴
txt └────┘ └──┘ └┘ └┘ ┴
par └────┘ └──┘ └┘ └┘ ┴
pid ┴ └┘ └┘ └┘ ┴
st ───────┘└─────┘└─────────┘└────────────────┘└───┘└──
220 have := @valid.nodup _ _ _ v bidx,
id ┴ └──┘
src └──────┘ └─────┘ ┴
typ └──────┘ └─────┘┴┴└──┘
doc └──────┘ └─────┘ ┴
txt └──────┘ └─────┘ ┴
par └──────┘ └─────┘ ┴
pid └───┘└─┘ └─────┘ ┴
st ────────────────────────────────────────┘└─
221 simp [hl, list.nodup_append] at this,
id └┘ └───────────────┘
src └────┘ └┘└───────────────┘└───────┘
typ └────┘└┘└┘└───────────────┘└───────┘
doc └────┘ └┘ └───────┘
txt └────┘ └┘ └───────┘
par └────┘ └┘ └───────┘
pid ┴┴ └┘ ┴┴└─────┘
st ───────────────────────────────────────────┘└─
222 simp [list.nodup_append, this, hvnd, djuv, djwv.symm] },
id └───────────────┘ └──┘ └──┘ └──┘
src └────┘└───────────────┘└┘ └┘ └┘ └┘ └┘
typ └────┘└───────────────┘└┘└──┘└┘└──┘└┘└──┘└┘└───────┘└┘
doc └────┘ └┘ └┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ └┘ └┘ ┴┴
st ─────────────────────────────────────────────────────────────┘└┘└
223 { rw [bkts', array.read_write_of_ne _ _ h], apply v.nodup } }
id └───┘ └────────────────────┘ ┴
src └──┘└───┘└┘└────────────────────┘└───┘ ┴ └────┘ ┴
typ └──┘└───┘└┘└────────────────────┘└───┘┴┴ └────┘ ┴
doc └──┘ └┘ └───┘ ┴ └────┘ ┴
txt └──┘ └┘ └───┘ ┴ └────┘ ┴
par └──┘ └┘ └───┘ ┴ └────┘ ┴
pid └┘ └┘ └───┘ ┴ ┴ ┴
st ────────────────┘└────────────────────────────┘└───────────────┘└───
224 end
st ────┘
225 end
226
227 theorem valid.replace_aux (a : α) (b : β a) : Π (l : list (Σ a, β a)), a ∈ l.map sigma.fst →
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴└──┘ └───────┘
src └──┘ ┴ ┴ ┴ └──┘ └───────┘
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴└──┘ └───────┘
228 ∃ (u w : list Σ a, β a) b', l = u ++ [⟨a, b'⟩] ++ w ∧ replace_aux a b l = u ++ [⟨a, b⟩] ++ w
id ┴ └──┘ ┴ ┴┴ ┴ ┴ └┘┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └─────────┘ ┴ └┘ ┴ ┴ └┘
typ ┴ └──┘ ┴ ┴┴ ┴ ┴ └┘┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴
doc └─────────┘
229 | [] := false.elim
id └┘ └────────┘
src └┘ └────────┘
typ └┘ └────────┘
230 | (⟨a', b'⟩::t) := begin
id └┘
src └┘
typ └┘
st └─────
231 by_cases e : a' = a,
id └┘ ┴ ┴
src └───────┘ └─┘ ┴┴┴
typ └───────┘ └─┘└┘┴┴┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ────────────────────┘└─
232 { subst a',
id └┘
src └────┘
typ └────┘└┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───┘└──────┘└─
233 suffices : ∃ (u w : list Σ a, β a) (b'' : β a),
id ┴ └──┘ ┴ ┴ ┴ ┴
src └─────────┘┴└──────┘└──┘┴┴└┘┴┴ ┴ └───────┘ ┴ ┴┴└
typ └─────────┘┴└──────┘└──┘┴┴└┘┴┴ ┴ └───────┘┴┴ ┴┴└
doc └─────────┘ └──────┘ ┴ └┘ ┴ ┴ └───────┘ ┴ ┴ └
txt └─────────┘ └──────┘ ┴ └┘ ┴ ┴ └───────┘ ┴ ┴ └
par └─────────┘ └──────┘ ┴ └┘ ┴ ┴ └───────┘ ┴ ┴ └
pid └───────┘└┘ └──────┘ ┴ └┘ ┴ ┴ └───────┘ ┴ ┴ └
st ────────────────────────────────────────────────────
234 (sigma.mk a b') :: t = u ++ ⟨a, b''⟩ :: w ∧
id └──────┘ └┘
src ─────┘ └──────┘┴ ┴ └┘ ┴ ┴ ┴ ┴└┘┴ └┘ └┘ ┴ ┴ └
typ ─────┘ └──────┘┴ ┴ └┘ ┴ ┴ ┴ ┴└┘┴ └┘ └┘ ┴ ┴ └
doc ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └
txt ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └
par ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └
pid ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └
st ──────────────────────────────────────────────────
235 replace_aux a b (⟨a, b'⟩ :: t) = u ++ ⟨a, b⟩ :: w, {simpa},
id └─────────┘ └┘ ┴ ┴ ┴
src ─────┘└─────────┘┴ ┴ ┴ └┘ └┘ ┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴ └───┘
typ ─────┘└─────────┘┴ ┴ ┴ └┘└┘└┘ ┴┴└┘ ┴ ┴ ┴ ┴└┘┴└┘ ┴ └───┘
doc ─────┘└─────────┘┴ ┴ ┴ └┘ └┘ ┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴ └───┘
txt ─────┘ ┴ ┴ ┴ └┘ └┘ ┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴ └───┘
par ─────┘ ┴ ┴ ┴ └┘ └┘ ┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴ └───┘
pid ─────┘ ┴ ┴ ┴ └┘ └┘ ┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴
st ──────────────────────────────────────────────────────┘└──────┘└┘└
236 refine ⟨[], t, b', _⟩, simp [replace_aux] },
id ┴ └┘ └─────────┘
src └─────┘ └┘ └┘ └──┘ └────┘└─────────┘└┘
typ └─────┘ └┘┴└┘└┘└──┘ └────┘└─────────┘└┘
doc └─────┘ └┘ └┘ └──┘ └────┘└─────────┘└┘
txt └─────┘ └┘ └┘ └──┘ └────┘ └┘
par └─────┘ └┘ └┘ └──┘ └────┘ └┘
pid ┴ └┘ └┘ └──┘ ┴┴ ┴┴
st ────────────────────────┘└───────────────────┘└┘└
237 { suffices : ∀ (x : β a) (_ : sigma.mk a x ∈ t), ∃ u w (b'' : β a),
id ┴ ┴ ┴ ┴
src └─────────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴┴┴ ┴ ┴┴└──────────┘ ┴ ┴┴└
typ └─────────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴┴┴ ┴ ┴┴└──────────┘┴┴ ┴┴└
doc └─────────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └
txt └─────────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └
par └─────────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └
pid └───────┘└┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └
st ──────────────────────────────────────────────────────────────────────
238 (sigma.mk a' b') :: t = u ++ ⟨a, b''⟩ :: w ∧
src ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └
typ ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └
doc ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └
txt ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └
par ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └
pid ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └
st ───────────────────────────────────────────────────
239 (sigma.mk a' b') :: (replace_aux a b t) = u ++ ⟨a, b⟩ :: w,
id └──────┘ └┘ └┘ └─────────┘ ┴ ┴ ┴
src ─────┘ └──────┘┴ ┴ └┘ ┴ └─────────┘┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴
typ ─────┘ └──────┘┴└┘┴└┘└┘ ┴ └─────────┘┴ ┴ ┴┴└┘ ┴ ┴ ┴ ┴└┘┴└┘ ┴
doc ─────┘ ┴ ┴ └┘ ┴ └─────────┘┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴
txt ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴
par ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴
pid ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴
st ───────────────────────────────────────────────────────────────┘└─
240 { simpa [replace_aux, ne.symm e, e] },
id └─────────┘ └─────┘ ┴ ┴
src └─────┘└─────────┘└┘└─────┘┴ └┘ └┘
typ └─────┘└─────────┘└┘└─────┘┴┴└┘┴└┘
doc └─────┘└─────────┘└┘ ┴ └┘ └┘
txt └─────┘ └┘ ┴ └┘ └┘
par └─────┘ └┘ ┴ └┘ └┘
pid ┴┴ └┘ ┴ └┘ ┴┴
st ─────┘└────────────────────────────────┘└┘└
241 intros x m,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └──┘
st ─────────────┘└─
242 have IH : ∀ (x : β a) (_ : sigma.mk a x ∈ t), ∃ u w (b'' : β a),
id └──────┘ ┴ ┴ ┴
src └────────┘ └────┘ ┴ └─────┘└──────┘┴ ┴ ┴ ┴ ┴ ┴┴└──────────┘ ┴ ┴┴└
typ └────────┘ └────┘ ┴ └─────┘└──────┘┴ ┴ ┴ ┴ ┴ ┴┴└──────────┘┴┴ ┴┴└
doc └────────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └
txt └────────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └
par └────────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └
pid └─────┘└─┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └
st ─────────────────────────────────────────────────────────────────────
243 t = u ++ ⟨a, b''⟩ :: w ∧ replace_aux a b t = u ++ ⟨a, b⟩ :: w,
id └─────────┘ ┴ ┴ ┴
src ─────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴└─────────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴
typ ─────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴└─────────┘┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴└┘┴└┘ ┴
doc ─────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴└─────────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴
txt ─────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴
par ─────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴
pid ─────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴
st ──────────────────────────────────────────────────────────────────┘└─
244 { simpa using valid.replace_aux t },
id └───────────────┘ ┴
src └──────────┘ ┴ ┴
typ └──────────┘└───────────────┘┴┴┴
doc └──────────┘ ┴ ┴
txt └──────────┘ ┴ ┴
par └──────────┘ ┴ ┴
pid ┴└────┘ ┴ ┴
st ─────┘└──────────────────────────────┘└┘└
245 rcases IH x m with ⟨u, w, b'', hl, hfl⟩,
id └┘ ┴ ┴
src └─────┘ ┴ ┴ └────────────────────────┘
typ └─────┘└┘┴┴┴┴└────────────────────────┘
doc └─────┘ ┴ ┴ └────────────────────────┘
txt └─────┘ ┴ ┴ └────────────────────────┘
par └─────┘ ┴ ┴ └────────────────────────┘
pid ┴ ┴ ┴ └────────────────────────┘
st ──────────────────────────────────────────┘└─
246 exact ⟨⟨a', b'⟩ :: u, w, b'', by simp [hl, hfl.symm, ne.symm e]⟩ }
id └┘ └┘ ┴ ┴ └─┘ └┘ └─────┘ ┴
src └────┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴└────┘ └┘ └┘└─────┘┴ ┴└┘
typ └────┘ └┘└┘└┘└┘ ┴┴└┘┴└┘└─┘└┘ ┴└────┘└┘└┘└──────┘└┘└─────┘┴┴┴└┘
doc └────┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴└────┘ └┘ └┘ ┴ ┴└┘
txt └────┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴└────┘ └┘ └┘ ┴ ┴└┘
par └────┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴└────┘ └┘ └┘ ┴ ┴└┘
pid ┴ └┘ └┘ ┴ └┘ └┘ └┘ └─────┘ └┘ └┘ ┴ └┘┴
st ───────────────────────────────────┘└─────────────────────────────┘└┘└─
247 end
st ──┘
248
249 theorem valid.replace {n : ℕ+}
id └┘
src └┘
typ └┘
doc └┘
250 {bkts : bucket_array α β n} {sz : ℕ} (a : α) (b : β a)
id └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────┘ ┴
typ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────────┘
251 (Hc : contains_aux a (bkts.read hash_fn a))
id └──────────┘ ┴ └──┘└───┘ └─────┘ ┴
src └──────────┘ └───┘
typ └──────────┘ ┴ └──┘└───┘ └─────┘ ┴
doc └──────────┘ └───┘
252 (v : valid bkts sz) : valid (bkts.modify hash_fn a (replace_aux a b)) sz :=
id └───┘ └──┘ └┘ └───┘ └──┘└─────┘ └─────┘ ┴ └─────────┘ ┴ ┴ └┘
src └───┘ └───┘ └─────┘ └─────────┘
typ └───┘ └──┘ └┘ └───┘ └──┘└─────┘ └─────┘ ┴ └─────────┘ ┴ ┴ └┘
doc └───┘ └───┘ └─────┘ └─────────┘
253 begin
st └─────
254 have nd := v.nodup (mk_idx n (hash_fn a)),
id └─────┘ └────┘ ┴ └─────┘ ┴
src └─────────┘└─────┘┴ └────┘┴ ┴ ┴ └┘
typ └─────────┘└─────┘┴ └────┘┴┴┴ └─────┘┴┴└┘
doc └─────────┘ ┴ └────┘┴ ┴ ┴ └┘
txt └─────────┘ ┴ ┴ ┴ ┴ └┘
par └─────────┘ ┴ ┴ ┴ ┴ └┘
pid └─────┘┴└─┘ ┴ ┴ ┴ ┴ └┘
st ──────────────────────────────────────────┘└─
255 rcases hash_map.valid.replace_aux a b (array.read bkts (mk_idx n (hash_fn a)))
id ┴ └────────┘ └──┘ └────┘ ┴ └─────┘ ┴
src └─────┘ ┴ ┴ ┴ └────────┘┴ ┴ └────┘┴ ┴ ┴ └───
typ └─────┘ ┴ ┴┴┴ └────────┘┴└──┘┴ └────┘┴┴┴ └─────┘┴┴└───
doc └─────┘ ┴ ┴ ┴ ┴ ┴ └────┘┴ ┴ ┴ └───
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
st ─────────────────────────────────────────────────────────────────────────────────
256 ((contains_aux_iff nd).1 Hc) with ⟨u, w, b', hl, hfl⟩,
id └──────────────┘ └┘ └┘
src ───┘ └──────────────┘┴ └──┘ └────────────────────────┘
typ ───┘ └──────────────┘┴└┘└──┘└┘└────────────────────────┘
doc ───┘ ┴ └──┘ └────────────────────────┘
txt ───┘ ┴ └──┘ └────────────────────────┘
par ───┘ ┴ └──┘ └────────────────────────┘
pid ───┘ ┴ └──┘ └────────────────────────┘
st ────────────────────────────────────────────────────────┘└─
257 simp [hl, list.nodup_append] at nd,
id └┘ └───────────────┘
src └────┘ └┘└───────────────┘└─────┘
typ └────┘└┘└┘└───────────────┘└─────┘
doc └────┘ └┘ └─────┘
txt └────┘ └┘ └─────┘
par └────┘ └┘ └─────┘
pid ┴┴ └┘ ┴┴└───┘
st ───────────────────────────────────┘└─
258 refine (v.modify hash_fn
id └──────┘ └─────┘
src └─────┘ └──────┘┴ └
typ └─────┘ └──────┘┴└─────┘└
doc └─────┘ ┴ └
txt └─────┘ ┴ └
par └─────┘ ┴ └
pid ┴ ┴ └
st ───────────────────────────
259 u [⟨a, b'⟩] [⟨a, b⟩] w hl hfl (list.nodup_singleton _)
id ┴ └┘ ┴ ┴ ┴ └┘ └─┘ └──────────────────┘
src ───┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └──────────────────┘└───
typ ───┘┴┴ └┘└┘┴ ┴ ┴└┘┴┴ ┴┴┴└┘┴└─┘┴ └──────────────────┘└───
doc ───┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └───
txt ───┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └───
par ───┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └───
pid ───┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └───
st ───────────────────────────────────────────────────────────
260 (λa' e, by simp at e; rw e)
id ┴
src ───┘ └────┘ ┴└───────┘└┘└─┘ └─
typ ───┘ └────┘ ┴└───────┘└┘└─┘┴└─
doc ───┘ └────┘ ┴└───────┘└┘└─┘ └─
txt ───┘ └────┘ ┴└───────┘└┘└─┘ └─
par ───┘ └────┘ ┴└───────┘└┘└─┘ └─
pid ───┘ └────┘ └─────────────┘ └─
st ─────────────┘└─────────────┘┴└─
261 (λa' e1 e2, _)
src ───┘ └────────────
typ ───┘ └────────────
doc ───┘ └────────────
txt ───┘ └────────────
par ───┘ └────────────
pid ───┘ └────────────
st ───────────────────
262 (λa' e1 e2, _)).2;
src ───┘ └─────────────┘
typ ───┘ └─────────────┘
doc ───┘ └─────────────┘
txt ───┘ └─────────────┘
par ───┘ └─────────────┘
pid ───┘ └───────────┘└┘
st ───────────────────────
263 { revert e1, simp [-sigma.exists] at e2, subst a', simp [nd] }
id └┘ └┘
src └───────┘ └────────────────────────┘ └────┘ └────┘ └┘
typ └───────┘ └────────────────────────┘ └────┘└┘ └────┘└┘└┘
doc └───────┘ └────────────────────────┘ └────┘ └────┘ └┘
txt └───────┘ └────────────────────────┘ └────┘ └────┘ └┘
par └───────┘ └────────────────────────┘ └────┘ └────┘ └┘
pid └─┘ ┴└─────────────┘┴└───┘ ┴ ┴┴ ┴┴
st ─┘└─────────┘└──────────────────────────┘└────────┘└──────────┘└─
264 end
st ──┘
265
266 theorem valid.insert {n : ℕ+}
id └┘
src └┘
typ └┘
doc └┘
267 {bkts : bucket_array α β n} {sz : ℕ} (a : α) (b : β a)
id └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────┘ ┴
typ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────────┘
268 (Hnc : ¬ contains_aux a (bkts.read hash_fn a))
id ┴ └──────────┘ ┴ └──┘└───┘ └─────┘ ┴
src ┴ └──────────┘ └───┘
typ ┴ └──────────┘ ┴ └──┘└───┘ └─────┘ ┴
doc └──────────┘ └───┘
269 (v : valid bkts sz) : valid (reinsert_aux bkts a b) (sz+1) :=
id └───┘ └──┘ └┘ └───┘ └──────────┘ └──┘ ┴ ┴ └┘┴
src └───┘ └───┘ └──────────┘ ┴
typ └───┘ └──┘ └┘ └───┘ └──────────┘ └──┘ ┴ ┴ └┘┴
doc └───┘ └───┘ └──────────┘
270 begin
st └─────
271 have nd := v.nodup (mk_idx n (hash_fn a)),
id └─────┘ └────┘ ┴ └─────┘ ┴
src └─────────┘└─────┘┴ └────┘┴ ┴ ┴ └┘
typ └─────────┘└─────┘┴ └────┘┴┴┴ └─────┘┴┴└┘
doc └─────────┘ ┴ └────┘┴ ┴ ┴ └┘
txt └─────────┘ ┴ ┴ ┴ ┴ └┘
par └─────────┘ ┴ ┴ ┴ ┴ └┘
pid └─────┘┴└─┘ ┴ ┴ ┴ ┴ └┘
st ──────────────────────────────────────────┘└─
272 refine (v.modify hash_fn
id └──────┘
src └─────┘ └──────┘┴ └
typ └─────┘ └──────┘┴ └
doc └─────┘ ┴ └
txt └─────┘ ┴ └
par └─────┘ ┴ └
pid ┴ ┴ └
st ───────────────────────────
273 [] [] [⟨a, b⟩] (bkts.read hash_fn a) rfl rfl (list.nodup_singleton _)
id ┴ └───────┘ └─────┘ ┴ └─┘ └──────────────────┘
src ───┘ ┴ ┴ └┘ ┴ ┴ └───────┘┴ ┴ └┘ ┴└─┘┴ └──────────────────┘└───
typ ───┘ ┴ ┴ └┘┴┴ ┴ └───────┘┴└─────┘┴┴└┘ ┴└─┘┴ └──────────────────┘└───
doc ───┘ ┴ ┴ └┘ ┴ ┴ └───────┘┴ ┴ └┘ ┴ ┴ └───
txt ───┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └───
par ───┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └───
pid ───┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └───
st ──────────────────────────────────────────────────────────────────────────
274 (λa' e, by simp at e; rw e)
id ┴
src ───┘ └────┘ ┴└───────┘└┘└─┘ └─
typ ───┘ └────┘ ┴└───────┘└┘└─┘┴└─
doc ───┘ └────┘ ┴└───────┘└┘└─┘ └─
txt ───┘ └────┘ ┴└───────┘└┘└─┘ └─
par ───┘ └────┘ ┴└───────┘└┘└─┘ └─
pid ───┘ └────┘ └─────────────┘ └─
st ─────────────┘└─────────────┘┴└─
275 (λa', false.elim)
id └────────┘
src ───┘ └──┘└────────┘└─
typ ───┘ └──┘└────────┘└─
doc ───┘ └──┘ └─
txt ───┘ └──┘ └─
par ───┘ └──┘ └─
pid ───┘ └──┘ └─
st ──────────────────────
276 (λa' e1 e2, _)).2,
src ───┘ └─────────────┘
typ ───┘ └─────────────┘
doc ───┘ └─────────────┘
txt ───┘ └─────────────┘
par ───┘ └─────────────┘
pid ───┘ └───────────┘└┘
st ────────────────────┘└─
277 simp [-sigma.exists] at e2, subst a',
id └┘
src └────────────────────────┘ └────┘
typ └────────────────────────┘ └────┘└┘
doc └────────────────────────┘ └────┘
txt └────────────────────────┘ └────┘
par └────────────────────────┘ └────┘
pid ┴└─────────────┘┴└───┘ ┴
st ───────────────────────────┘└────────┘└─
278 exact Hnc ((contains_aux_iff nd).2 e1)
id └─┘ └──────────────┘ └┘ └┘
src └────┘ ┴ └──────────────┘┴ └──┘ └┘
typ └────┘└─┘┴ └──────────────┘┴└┘└──┘└┘└┘
doc └────┘ ┴ ┴ └──┘ └┘
txt └────┘ ┴ ┴ └──┘ └┘
par └────┘ ┴ ┴ └──┘ └┘
pid ┴ ┴ ┴ └──┘ ┴┴
st ────────────────────────────────────────┘
279 end
st └─┘
280
281 theorem valid.erase_aux (a : α) : Π (l : list (Σ a, β a)), a ∈ l.map sigma.fst →
id ┴ ┴ └──┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴└──┘ └───────┘
src └──┘ ┴ ┴ ┴ └──┘ └───────┘
typ ┴ ┴ └──┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴└──┘ └───────┘
282 ∃ (u w : list Σ a, β a) b, l = u ++ [⟨a, b⟩] ++ w ∧ erase_aux a l = u ++ [] ++ w
id ┴ └──┘ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └┘ └┘ └┘ ┴
src ┴ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └───────┘ ┴ └┘ └┘ └┘
typ ┴ └──┘ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └┘ └┘ └┘ ┴
doc └───────┘
283 | [] := false.elim
id └┘ └────────┘
src └┘ └────────┘
typ └┘ └────────┘
284 | (⟨a', b'⟩::t) := begin
id └┘
src └┘
typ └┘
st └─────
285 by_cases e : a' = a,
id └┘ ┴ ┴
src └───────┘ └─┘ ┴┴┴
typ └───────┘ └─┘└┘┴┴┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ────────────────────┘└─
286 { subst a',
id └┘
src └────┘
typ └────┘└┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───┘└──────┘└─
287 simpa [erase_aux, and_comm] using show ∃ u w (x : β a),
id └───────┘ └──────┘ ┴ ┴ ┴
src └─────┘└───────┘└┘└──────┘└──────┘ ┴┴└────────┘ ┴ ┴┴└
typ └─────┘└───────┘└┘└──────┘└──────┘ ┴┴└────────┘┴┴ ┴┴└
doc └─────┘└───────┘└┘ └──────┘ ┴ └────────┘ ┴ ┴ └
txt └─────┘ └┘ └──────┘ ┴ └────────┘ ┴ ┴ └
par └─────┘ └┘ └──────┘ ┴ └────────┘ ┴ ┴ └
pid ┴┴ └┘ ┴┴└────┘ ┴ └────────┘ ┴ ┴ └
st ────────────────────────────────────────────────────────────
288 t = u ++ w ∧ (sigma.mk a b') :: t = u ++ ⟨a, x⟩ :: w,
id └┘ └──────┘ ┴
src ─────┘ ┴ ┴ ┴└┘┴ ┴ ┴ └──────┘┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └─
typ ─────┘ ┴ ┴ ┴└┘┴ ┴ ┴ └──────┘┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴└┘ └┘ ┴ └─
doc ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └─
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └─
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └─
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └─
st ────────────────────────────────────────────────────────────
289 from ⟨[], t, b', by simp⟩ },
id └┘ ┴ └┘
src ──────────┘ └┘└┘ └┘ └┘ ┴└──┘└┘
typ ──────────┘ └┘└┘┴└┘└┘└┘ ┴└──┘└┘
doc ──────────┘ └┘ └┘ └┘ ┴└──┘└┘
txt ──────────┘ └┘ └┘ └┘ ┴└──┘└┘
par ──────────┘ └┘ └┘ └┘ ┴└──┘└┘
pid ──────────┘ └┘ └┘ └┘ └────┘┴
st ────────────────────────┘└───┘└┘└┘└
290 { simp [erase_aux, e, ne.symm e],
id └───────┘ ┴ └─────┘ ┴
src └────┘└───────┘└┘ └┘└─────┘┴ ┴
typ └────┘└───────┘└┘┴└┘└─────┘┴┴┴
doc └────┘└───────┘└┘ └┘ ┴ ┴
txt └────┘ └┘ └┘ ┴ ┴
par └────┘ └┘ └┘ ┴ ┴
pid ┴┴ └┘ └┘ ┴ ┴
st ─────────────────────────────────┘└─
291 suffices : ∀ (b : β a) (_ : sigma.mk a b ∈ t), ∃ u w (x : β a),
id ┴ ┴ ┴ ┴
src └─────────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴┴┴ ┴ ┴┴└────────┘ ┴ ┴┴└
typ └─────────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴┴┴ ┴ ┴┴└────────┘┴┴ ┴┴└
doc └─────────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ └
txt └─────────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ └
par └─────────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ └
pid └───────┘└┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ └
st ────────────────────────────────────────────────────────────────────
292 (sigma.mk a' b') :: t = u ++ ⟨a, x⟩ :: w ∧
src ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └
typ ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └
doc ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └
txt ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └
par ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └
pid ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └
st ─────────────────────────────────────────────────
293 (sigma.mk a' b') :: (erase_aux a t) = u ++ w,
id └──────┘ └┘ └┘ └───────┘ ┴ ┴
src ─────┘ └──────┘┴ ┴ └┘ ┴ └───────┘┴ ┴ └┘ ┴ ┴ ┴
typ ─────┘ └──────┘┴└┘┴└┘└┘ ┴ └───────┘┴┴┴┴└┘ ┴ ┴ ┴
doc ─────┘ ┴ ┴ └┘ ┴ └───────┘┴ ┴ └┘ ┴ ┴ ┴
txt ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
par ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
pid ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────┘└─
294 { simpa [replace_aux, ne.symm e, e] },
id └─────────┘ └─────┘ ┴ ┴
src └─────┘└─────────┘└┘└─────┘┴ └┘ └┘
typ └─────┘└─────────┘└┘└─────┘┴┴└┘┴└┘
doc └─────┘└─────────┘└┘ ┴ └┘ └┘
txt └─────┘ └┘ ┴ └┘ └┘
par └─────┘ └┘ ┴ └┘ └┘
pid ┴┴ └┘ ┴ └┘ ┴┴
st ─────┘└────────────────────────────────┘└┘└
295 intros b m,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └──┘
st ─────────────┘└─
296 have IH : ∀ (x : β a) (_ : sigma.mk a x ∈ t), ∃ u w (x : β a),
id └──────┘ ┴ ┴ ┴
src └────────┘ └────┘ ┴ └─────┘└──────┘┴ ┴ ┴ ┴ ┴ ┴┴└────────┘ ┴ ┴┴└
typ └────────┘ └────┘ ┴ └─────┘└──────┘┴ ┴ ┴ ┴ ┴ ┴┴└────────┘┴┴ ┴┴└
doc └────────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ └
txt └────────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ └
par └────────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ └
pid └─────┘└─┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ └
st ───────────────────────────────────────────────────────────────────
297 t = u ++ ⟨a, x⟩ :: w ∧ erase_aux a t = u ++ w,
id └───────┘ ┴ ┴
src ─────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴└───────┘┴ ┴ ┴ ┴ ┴ ┴
typ ─────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴└───────┘┴┴┴┴┴ ┴ ┴ ┴
doc ─────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴└───────┘┴ ┴ ┴ ┴ ┴ ┴
txt ─────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par ─────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ─────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────┘└─
298 { simpa using valid.erase_aux t },
id └─────────────┘ ┴
src └──────────┘ ┴ ┴
typ └──────────┘└─────────────┘┴┴┴
doc └──────────┘ ┴ ┴
txt └──────────┘ ┴ ┴
par └──────────┘ ┴ ┴
pid ┴└────┘ ┴ ┴
st ─────┘└────────────────────────────┘└┘└
299 rcases IH b m with ⟨u, w, b'', hl, hfl⟩,
id └┘ ┴ ┴
src └─────┘ ┴ ┴ └────────────────────────┘
typ └─────┘└┘┴┴┴┴└────────────────────────┘
doc └─────┘ ┴ ┴ └────────────────────────┘
txt └─────┘ ┴ ┴ └────────────────────────┘
par └─────┘ ┴ ┴ └────────────────────────┘
pid ┴ ┴ ┴ └────────────────────────┘
st ──────────────────────────────────────────┘└─
300 exact ⟨⟨a', b'⟩ :: u, w, b'', by simp [hl, hfl.symm]⟩ }
id └┘ └┘ ┴ ┴ └─┘ └┘
src └────┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴└────┘ └┘ ┴└┘
typ └────┘ └┘└┘└┘└┘ ┴┴└┘┴└┘└─┘└┘ ┴└────┘└┘└┘└──────┘┴└┘
doc └────┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴└────┘ └┘ ┴└┘
txt └────┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴└────┘ └┘ ┴└┘
par └────┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴└────┘ └┘ ┴└┘
pid ┴ └┘ └┘ ┴ └┘ └┘ └┘ └─────┘ └┘ └┘┴
st ───────────────────────────────────┘└──────────────────┘└┘└─
301 end
st ──┘
302
303 theorem valid.erase {n} {bkts : bucket_array α β n} {sz}
id └──────────┘ ┴ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴ ┴
doc └──────────┘
304 (a : α) (Hc : contains_aux a (bkts.read hash_fn a))
id ┴ └──────────┘ ┴ └──┘└───┘ └─────┘ ┴
src └──────────┘ └───┘
typ ┴ └──────────┘ ┴ └──┘└───┘ └─────┘ ┴
doc └──────────┘ └───┘
305 (v : valid bkts sz) : valid (bkts.modify hash_fn a (erase_aux a)) (sz-1) :=
id └───┘ └──┘ └┘ └───┘ └──┘└─────┘ └─────┘ ┴ └───────┘ ┴ └┘┴
src └───┘ └───┘ └─────┘ └───────┘ ┴
typ └───┘ └──┘ └┘ └───┘ └──┘└─────┘ └─────┘ ┴ └───────┘ ┴ └┘┴
doc └───┘ └───┘ └─────┘ └───────┘
306 begin
st └─────
307 have nd := v.nodup (mk_idx n (hash_fn a)),
id └─────┘ └────┘ ┴ └─────┘ ┴
src └─────────┘└─────┘┴ └────┘┴ ┴ ┴ └┘
typ └─────────┘└─────┘┴ └────┘┴┴┴ └─────┘┴┴└┘
doc └─────────┘ ┴ └────┘┴ ┴ ┴ └┘
txt └─────────┘ ┴ ┴ ┴ ┴ └┘
par └─────────┘ ┴ ┴ ┴ ┴ └┘
pid └─────┘┴└─┘ ┴ ┴ ┴ ┴ └┘
st ──────────────────────────────────────────┘└─
308 rcases hash_map.valid.erase_aux a (array.read bkts (mk_idx n (hash_fn a)))
id └────────┘ └──┘ └────┘ ┴ └─────┘ ┴
src └─────┘ ┴ ┴ └────────┘┴ ┴ └────┘┴ ┴ ┴ └───
typ └─────┘ ┴ ┴ └────────┘┴└──┘┴ └────┘┴┴┴ └─────┘┴┴└───
doc └─────┘ ┴ ┴ ┴ ┴ └────┘┴ ┴ ┴ └───
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
st ─────────────────────────────────────────────────────────────────────────────
309 ((contains_aux_iff nd).1 Hc) with ⟨u, w, b, hl, hfl⟩,
id └──────────────┘ └┘ └┘
src ───┘ └──────────────┘┴ └──┘ └───────────────────────┘
typ ───┘ └──────────────┘┴└┘└──┘└┘└───────────────────────┘
doc ───┘ ┴ └──┘ └───────────────────────┘
txt ───┘ ┴ └──┘ └───────────────────────┘
par ───┘ ┴ └──┘ └───────────────────────┘
pid ───┘ ┴ └──┘ └───────────────────────┘
st ───────────────────────────────────────────────────────┘└─
310 refine (v.modify hash_fn u [⟨a, b⟩] [] w hl hfl list.nodup_nil _ _ _).2;
id └──────┘ └─────┘ ┴ ┴ ┴ ┴ └┘ └─┘ └────────────┘
src └─────┘ └──────┘┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴└────────────┘└───────┘
typ └─────┘ └──────┘┴└─────┘┴┴┴ ┴└┘┴┴ ┴ ┴┴┴└┘┴└─┘┴└────────────┘└───────┘
doc └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘
txt └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘
par └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘
pid ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘└┘
st ───────────────────────────────────────────────────────────────────────────
311 { intros, simp at *; contradiction }
src └────┘ └───────┘ └────────────┘
typ └────┘ └───────┘ └────────────┘
doc └────┘ └───────┘ └────────────┘
txt └────┘ └───────┘ └────────────┘
par └────┘ └───────┘ └────────────┘
pid ┴└──┘ ┴
st ─┘└──────┘└─────────────────────────┘└─
312 end
st ──┘
313
314 end
315 end hash_map
316
317 /-- A hash map data structure, representing a finite key-value map
318 with key type `α` and value type `β` (which may depend on `α`). -/
319 structure hash_map (α : Type u) [decidable_eq α] (β : α → Type v) :=
id └──┘ └──────────┘ ┴ ┴ ┴
src └──────────┘
typ └──┘ └──────────┘ ┴ ┴ ┴
320 (hash_fn : α → nat)
id ┴ ┴ └─┘
src └─┘
typ ┴ ┴ └─┘
321 (size : ℕ)
id ┴
src ┴
typ ┴
322 (nbuckets : ℕ+)
id └┘
src └┘
typ └┘
doc └┘
323 (buckets : bucket_array α β nbuckets)
id └──────────┘ ┴ ┴ └──────┘
src └──────────┘
typ └──────────┘ ┴ ┴ └──────┘
doc └──────────┘
324 (is_valid : hash_map.valid hash_fn buckets size)
id └────────────┘ └─────┘ └─────┘ └──┘
src └────────────┘
typ └────────────┘ └─────┘ └─────┘ └──┘
doc └────────────┘
325
326 /-- Construct an empty hash map with buffer size `nbuckets` (default 8). -/
327 def mk_hash_map {α : Type u} [decidable_eq α] {β : α → Type v} (hash_fn : α → nat) (nbuckets := 8) : hash_map α β :=
id └──────────┘ ┴ ┴ ┴ └─┘ ┴ └──────┘ ┴ ┴
src └──────────┘ └─┘ ┴ └──────┘
typ └──────────┘ ┴ ┴ ┴ └─┘ ┴ └──────┘ ┴ ┴
doc ┴ └──────┘
328 let n := if nbuckets = 0 then 8 else nbuckets in
id ┴ └──────┘ ┴ └──────┘
src ┴
typ ┴ └──────┘ ┴ └──────┘
329 let nz : n > 0 := by abstract { cases nbuckets; simp [if_pos, nat.succ_ne_zero] } in
id ┴ ┴ └──────┘ └────┘ └──────────────┘
src ┴ └─────────┘└────┘ └┘└────┘└────┘└┘└──────────────┘└┘└┘
typ ┴ ┴ └─────────┘└────┘└──────┘└┘└────┘└────┘└┘└──────────────┘└┘└┘
doc └─────────┘└────┘ └┘└────┘ └┘ └┘└┘
txt └─────────┘└────┘ └┘└────┘ └┘ └┘└┘
par └─────────┘└────┘ └┘└────┘ └┘ └┘└┘
pid ┴└──────┘ └──────┘ └┘ └─┘┴
st └─────────┘└───────────────────────────────────────────────┘┴┴
330 { hash_fn := hash_fn,
id └─────┘
typ └─────┘
331 size := 0,
332 nbuckets := ⟨n, nz⟩,
id ┴ └┘
typ ┴ └┘
333 buckets := mk_array n [],
id └──────┘ ┴ └┘
src └──────┘ └┘
typ └──────┘ ┴ └┘
334 is_valid := hash_map.mk_valid _ _ }
id └───────────────┘
src └───────────────┘
typ └───────────────┘
335
336 namespace hash_map
337 variables {α : Type u} {β : α → Type v} [decidable_eq α]
id ┴ └──────────┘
src └──────────┘
typ ┴ └──────────┘
338
339 /-- Return the value corresponding to a key, or `none` if not found -/
340 def find (m : hash_map α β) (a : α) : option (β a) :=
id └──────┘ ┴ ┴ ┴ └────┘ ┴ ┴
src └──────┘ └────┘
typ └──────┘ ┴ ┴ ┴ └────┘ ┴ ┴
doc └──────┘
341 find_aux a (m.buckets.read m.hash_fn a)
id └──────┘ ┴ ┴└──────┘└───┘ ┴└──────┘ ┴
src └──────┘ └──────┘└───┘ └──────┘
typ └──────┘ ┴ ┴└──────┘└───┘ ┴└──────┘ ┴
doc └──────┘ └───┘
342
343 /-- Return `tt` if the key exists in the map -/
344 def contains (m : hash_map α β) (a : α) : bool :=
id └──────┘ ┴ ┴ ┴ └──┘
src └──────┘ └──┘
typ └──────┘ ┴ ┴ ┴ └──┘
doc └──────┘
345 (m.find a).is_some
id ┴└───┘ ┴ └─────┘
src └───┘ └─────┘
typ ┴└───┘ ┴ └─────┘
doc └───┘
346
347 instance : has_mem α (hash_map α β) := ⟨λa m, m.contains a⟩
id └─────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴└───────┘ ┴
src └─────┘ └──────┘ └───────┘
typ └─────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴└───────┘ ┴
doc └──────┘ └───────┘
348
349 /-- Fold a function over the key-value pairs in the map -/
350 def fold {δ : Type w} (m : hash_map α β) (d : δ) (f : δ → Π a, β a → δ) : δ :=
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────┘
351 m.buckets.foldl d f
id ┴└──────┘└────┘ ┴ ┴
src └──────┘└────┘
typ ┴└──────┘└────┘ ┴ ┴
doc └────┘
352
353 /-- The list of key-value pairs in the map -/
354 def entries (m : hash_map α β) : list Σ a, β a :=
id └──────┘ ┴ ┴ └──┘ ┴ ┴┴ ┴ ┴
src └──────┘ └──┘ ┴ ┴
typ └──────┘ ┴ ┴ └──┘ ┴ ┴┴ ┴ ┴
doc └──────┘
355 m.buckets.as_list
id ┴└──────┘└──────┘
src └──────┘└──────┘
typ ┴└──────┘└──────┘
doc └──────┘
356
357 /-- The list of keys in the map -/
358 def keys (m : hash_map α β) : list α :=
id └──────┘ ┴ ┴ └──┘ ┴
src └──────┘ └──┘
typ └──────┘ ┴ ┴ └──┘ ┴
doc └──────┘
359 m.entries.map sigma.fst
id ┴└──────┘└──┘ └───────┘
src └──────┘└──┘ └───────┘
typ ┴└──────┘└──┘ └───────┘
doc └──────┘
360
361 theorem find_iff (m : hash_map α β) (a : α) (b : β a) :
id └──────┘ ┴ ┴ ┴ ┴ ┴
src └──────┘
typ └──────┘ ┴ ┴ ┴ ┴ ┴
doc └──────┘
362 m.find a = some b ↔ sigma.mk a b ∈ m.entries :=
id ┴└───┘ ┴ ┴ └──┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴└──────┘
src └───┘ ┴ └──┘ ┴ └──────┘ ┴ └──────┘
typ ┴└───┘ ┴ ┴ └──┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴└──────┘
doc └───┘ └──────┘
363 m.is_valid.find_aux_iff _
id ┴└───────┘└───────────┘
src └───────┘└───────────┘
typ ┴└───────┘└───────────┘
364
365 theorem contains_iff (m : hash_map α β) (a : α) :
id └──────┘ ┴ ┴ ┴
src └──────┘
typ └──────┘ ┴ ┴ ┴
doc └──────┘
366 m.contains a ↔ a ∈ m.keys :=
id ┴└───────┘ ┴ ┴ ┴ ┴ ┴└───┘
src └───────┘ ┴ ┴ └───┘
typ ┴└───────┘ ┴ ┴ ┴ ┴ ┴└───┘
doc └───────┘ └───┘
367 m.is_valid.contains_aux_iff _ _
id ┴└───────┘└───────────────┘
src └───────┘└───────────────┘
typ ┴└───────┘└───────────────┘
368
369 theorem entries_empty (hash_fn : α → nat) (n) :
id ┴ └─┘
src └─┘
typ ┴ └─┘
370 (@mk_hash_map α _ β hash_fn n).entries = [] :=
id └─────────┘ ┴ ┴ └─────┘ ┴ └─────┘ ┴ └┘
src └─────────┘ └─────┘ ┴ └┘
typ └─────────┘ ┴ ┴ └─────┘ ┴ └─────┘ ┴ └┘
doc └─────────┘ └─────┘
371 by dsimp [entries, mk_hash_map]; rw mk_as_list
id └─────┘ └─────────┘ └────────┘
src └─────┘└─────┘└┘└─────────┘┴ └─┘└────────┘└
typ └─────┘└─────┘└┘└─────────┘┴ └─┘└────────┘└
doc └─────┘└─────┘└┘└─────────┘┴ └─┘ └
txt └─────┘ └┘ ┴ └─┘ └
par └─────┘ └┘ ┴ └─┘ └
pid ┴┴ └┘ ┴ ┴ └
st └────────────────────────────────┘└────────┘└
372
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
373 theorem keys_empty (hash_fn : α → nat) (n) :
id ┴ └─┘
src └─┘
typ ┴ └─┘
374 (@mk_hash_map α _ β hash_fn n).keys = [] :=
id └─────────┘ ┴ ┴ └─────┘ ┴ └──┘ ┴ └┘
src └─────────┘ └──┘ ┴ └┘
typ └─────────┘ ┴ ┴ └─────┘ ┴ └──┘ ┴ └┘
doc └─────────┘ └──┘
375 by dsimp [keys]; rw entries_empty; refl
id └──┘ └───────────┘
src └─────┘└──┘┴ └─┘└───────────┘ └────
typ └─────┘└──┘┴ └─┘└───────────┘ └────
doc └─────┘└──┘┴ └─┘ └────
txt └─────┘ ┴ └─┘ └────
par └─────┘ ┴ └─┘ └────
pid ┴┴ ┴ ┴ └
st └────────────────┘└───────────┘└──────
376
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
377 theorem find_empty (hash_fn : α → nat) (n a) :
id ┴ └─┘
src └─┘
typ ┴ └─┘
378 (@mk_hash_map α _ β hash_fn n).find a = none :=
id └─────────┘ ┴ ┴ └─────┘ ┴ └──┘ ┴ ┴ └──┘
src └─────────┘ └──┘ ┴ └──┘
typ └─────────┘ ┴ ┴ └─────┘ ┴ └──┘ ┴ ┴ └──┘
doc └─────────┘ └──┘
379 by induction h : (@mk_hash_map α _ β hash_fn n).find a; [refl,
id └─────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴
src └────────┘ └─┘ └─────────┘┴ └─┘ ┴ ┴ └─────┘ ┴└──┘
typ └────────┘ └─┘ └─────────┘┴┴└─┘┴┴└─────┘┴┴└─────┘┴ ┴└──┘
doc └────────┘ └─┘ └─────────┘┴ └─┘ ┴ ┴ └─────┘ └──┘
txt └────────┘ └─┘ ┴ └─┘ ┴ ┴ └─────┘ └──┘
par └────────┘ └─┘ ┴ └─┘ ┴ ┴ └─────┘ └──┘
pid ┴ └─┘ ┴ └─┘ ┴ ┴ └─────┘
st └────────────────────────────────────────────────────────────
380 { have := (find_iff _ _ _).1 h, rw entries_empty at this, contradiction }]
id └──────┘ ┴ └───────────┘
src └──────┘ └──────┘└────────┘ └─┘└───────────┘└──────┘ └────────────┘
typ └──────┘ └──────┘└────────┘┴ └─┘└───────────┘└──────┘ └────────────┘
doc └──────┘ └────────┘ └─┘ └──────┘ └────────────┘
txt └──────┘ └────────┘ └─┘ └──────┘ └────────────┘
par └──────┘ └────────┘ └─┘ └──────┘ └────────────┘
pid └───┘└─┘ └────────┘ ┴ └──────┘ ┴
st ──┘└────────────────────────────┘└────────────────────────┘└──────────────┘└┘
381
382 theorem not_contains_empty (hash_fn : α → nat) (n a) :
id ┴ └─┘
src └─┘
typ ┴ └─┘
383 ¬ (@mk_hash_map α _ β hash_fn n).contains a :=
id ┴ └─────────┘ ┴ ┴ └─────┘ ┴ └──────┘ ┴
src ┴ └─────────┘ └──────┘
typ ┴ └─────────┘ ┴ ┴ └─────┘ ┴ └──────┘ ┴
doc └─────────┘ └──────┘
384 by apply bool_iff_false.2; dsimp [contains]; rw [find_empty]; refl
id └────────────┘ └──────┘ └────────┘
src └────┘└────────────┘└┘ └─────┘└──────┘┴ └──┘└────────┘┴ └────
typ └────┘└────────────┘└┘ └─────┘└──────┘┴ └──┘└────────┘┴ └────
doc └────┘ └┘ └─────┘└──────┘┴ └──┘ ┴ └────
txt └────┘ └┘ └─────┘ ┴ └──┘ ┴ └────
par └────┘ └┘ └─────┘ ┴ └──┘ ┴ └────
pid ┴ └┘ ┴┴ ┴ └┘ ┴ └
st └─────────────────────────────────────────────┘└────────┘┴└──────
385
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
386 theorem insert_lemma (hash_fn : α → nat) {n n'}
id ┴ └─┘
src └─┘
typ ┴ └─┘
387 {bkts : bucket_array α β n} {sz} (v : valid hash_fn bkts sz) :
id └──────────┘ ┴ ┴ ┴ └───┘ └─────┘ └──┘ └┘
src └──────────┘ └───┘
typ └──────────┘ ┴ ┴ ┴ └───┘ └─────┘ └──┘ └┘
doc └──────────┘ └───┘
388 valid hash_fn (bkts.foldl (mk_array _ [] : bucket_array α β n') (reinsert_aux hash_fn)) sz :=
id └───┘ └─────┘ └──┘└────┘ └──────┘ └┘ └──────────┘ ┴ ┴ └┘ └──────────┘ └─────┘ └┘
src └───┘ └────┘ └──────┘ └┘ └──────────┘ └──────────┘
typ └───┘ └─────┘ └──┘└────┘ └──────┘ └┘ └──────────┘ ┴ ┴ └┘ └──────────┘ └─────┘ └┘
doc └───┘ └────┘ └──────────┘ └──────────┘
389 begin
st └─────
390 suffices : ∀ (l : list Σ a, β a) (t : bucket_array α β n') sz,
id └──┘ ┴ └──────────┘ ┴ └┘
src └─────────┘ └────┘└──┘┴ └┘ ┴ ┴ └─────┘└──────────┘┴ ┴ ┴ └──┘ └
typ └─────────┘ └────┘└──┘┴ └┘ ┴┴┴ └─────┘└──────────┘┴┴┴ ┴└┘└──┘ └
doc └─────────┘ └────┘ ┴ └┘ ┴ ┴ └─────┘└──────────┘┴ ┴ ┴ └──┘ └
txt └─────────┘ └────┘ ┴ └┘ ┴ ┴ └─────┘ ┴ ┴ ┴ └──┘ └
par └─────────┘ └────┘ ┴ └┘ ┴ ┴ └─────┘ ┴ ┴ ┴ └──┘ └
pid └───────┘└┘ └────┘ ┴ └┘ ┴ ┴ └─────┘ ┴ ┴ ┴ └──┘ └
st ─────────────────────────────────────────────────────────────────
391 valid hash_fn t sz → ((l ++ t.as_list).map sigma.fst).nodup →
id └───┘ └┘ └──────┘ └───────┘
src ───┘ ┴ ┴ ┴ ┴ ┴ ┴└┘┴ └──────┘└────┘└───────┘└──────┘ └
typ ───┘└───┘┴ ┴ ┴ ┴ ┴ ┴└┘┴ └──────┘└────┘└───────┘└──────┘ └
doc ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘└────┘ └──────┘ └
txt ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └──────┘ └
par ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └──────┘ └
pid ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └──────┘ └
st ──────────────────────────────────────────────────────────────────
392 valid hash_fn (l.foldl (λr (a : Σ a, β a), reinsert_aux hash_fn r a.1 a.2) t) (sz + l.length),
id └───┘ └────┘ ┴ ┴ ┴ └──────────┘ └─────┘ ┴ └─────┘
src ───┘└───┘┴ ┴ └────┘┴ └─────┘┴└┘┴┴ ┴ └─┘└──────────┘┴ ┴ ┴ └─┘ └──┘ └┘ ┴┴┴ └─────┘┴
typ ───┘└───┘┴ ┴ └────┘┴ └─────┘┴└┘┴┴┴┴ └─┘└──────────┘┴└─────┘┴ ┴ └─┘ └──┘ └┘ ┴┴┴ └─────┘┴
doc ───┘└───┘┴ ┴ ┴ └─────┘ └┘ ┴ ┴ └─┘└──────────┘┴ ┴ ┴ └─┘ └──┘ └┘ ┴ ┴ ┴
txt ───┘ ┴ ┴ ┴ └─────┘ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ └──┘ └┘ ┴ ┴ ┴
par ───┘ ┴ ┴ ┴ └─────┘ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ └──┘ └┘ ┴ ┴ ┴
pid ───┘ ┴ ┴ ┴ └─────┘ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ └──┘ └┘ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
393 { have p := this bkts.as_list _ _ (mk_valid _ _),
id └──┘ └──────────┘ └──────┘
src └────────┘ ┴└──────────┘└───┘ └──────┘└───┘
typ └────────┘└──┘┴└──────────┘└───┘ └──────┘└───┘
doc └────────┘ ┴└──────────┘└───┘ └───┘
txt └────────┘ ┴ └───┘ └───┘
par └────────┘ ┴ └───┘ └───┘
pid └────┘┴└─┘ ┴ └───┘ └───┘
st ───┘└────────────────────────────────────────────┘└─
394 rw [mk_as_list, list.append_nil, zero_add, v.len] at p,
id └────────┘ └─────────────┘ └──────┘
src └──┘└────────┘└┘└─────────────┘└┘└──────┘└┘ └────┘
typ └──┘└────────┘└┘└─────────────┘└┘└──────┘└┘└───┘└────┘
doc └──┘ └┘ └┘ └┘ └────┘
txt └──┘ └┘ └┘ └┘ └────┘
par └──┘ └┘ └┘ └┘ └────┘
pid └┘ └┘ └┘ └┘ ┴└───┘
st ─────────────────┘└───────────────┘└────────┘└─────┘┴└───┘└─
395 rw bucket_array.foldl_eq,
id └───────────────────┘
src └─┘└───────────────────┘
typ └─┘└───────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────────────────┘└─
396 exact p (v.as_list_nodup _) },
id ┴ └─────────────┘
src └────┘ ┴ └─────────────┘└──┘
typ └────┘┴┴ └─────────────┘└──┘
doc └────┘ ┴ └──┘
txt └────┘ ┴ └──┘
par └────┘ ┴ └──┘
pid ┴ ┴ └─┘┴
st ───────────────────────────────┘└┘└
397 intro l, induction l with c l IH; intros t sz v nd, {exact v},
id ┴ ┴
src └─────┘ └────────┘ └──────────┘ └──────────────┘ └────┘
typ └─────┘ └────────┘┴└──────────┘ └──────────────┘ └────┘┴
doc └─────┘ └────────┘ └──────────┘ └──────────────┘ └────┘
txt └─────┘ └────────┘ └──────────┘ └──────────────┘ └────┘
par └─────┘ └────────┘ └──────────┘ └──────────────┘ └────┘
pid └┘ ┴ ┴└─────────┘ └────────┘ ┴
st ────────┘└─────────────────────────────────────────┘└────────┘└┘└
398 rw show sz + (c :: l).length = sz + 1 + l.length, by simp,
id ┴ ┴ └┘ └──────┘
src └─┘ ┴ ┴ ┴ ┴ ┴ └───────┘┴┴ ┴ └─┘ ┴└──────┘└───┘└──┘
typ └─┘ ┴ ┴ ┴ ┴┴ ┴ └───────┘┴┴└┘┴ └─┘ ┴└──────┘└───┘└──┘
doc └─┘ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └─┘ ┴ └───┘└──┘
txt └─┘ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └─┘ ┴ └───┘└──┘
par └─┘ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └─┘ ┴ └───┘└──┘
pid ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └─┘ ┴ └───────┘
st ─────────────────────────────────────────────────────┘└───┘└─
399 rcases (show (l.map sigma.fst).nodup ∧
id ┴
src └─────┘ ┴ ┴ └──────┘┴└
typ └─────┘ ┴ ┴ └──────┘┴└
doc └─────┘ ┴ ┴ └──────┘ └
txt └─────┘ ┴ ┴ └──────┘ └
par └─────┘ ┴ ┴ └──────┘ └
pid ┴ ┴ ┴ └──────┘ └
st ─────────────────────────────────────────
400 ((bucket_array.as_list t).map sigma.fst).nodup ∧
src ─────┘ ┴ └────┘ └──────┘ └
typ ─────┘ ┴ └────┘ └──────┘ └
doc ─────┘ ┴ └────┘ └──────┘ └
txt ─────┘ ┴ └────┘ └──────┘ └
par ─────┘ ┴ └────┘ └──────┘ └
pid ─────┘ ┴ └────┘ └──────┘ └
st ───────────────────────────────────────────────────────
401 c.fst ∉ l.map sigma.fst ∧
id ┴
src ─────┘ ┴┴┴ ┴ ┴ └
typ ─────┘ ┴┴┴ ┴ ┴ └
doc ─────┘ ┴ ┴ ┴ ┴ └
txt ─────┘ ┴ ┴ ┴ ┴ └
par ─────┘ ┴ ┴ ┴ ┴ └
pid ─────┘ ┴ ┴ ┴ ┴ └
st ────────────────────────────────
402 c.fst ∉ (bucket_array.as_list t).map sigma.fst ∧
id └───┘
src ─────┘└───┘┴ ┴ ┴ └────┘ ┴ └
typ ─────┘└───┘┴ ┴ ┴ └────┘ ┴ └
doc ─────┘ ┴ ┴ ┴ └────┘ ┴ └
txt ─────┘ ┴ ┴ ┴ └────┘ ┴ └
par ─────┘ ┴ ┴ ┴ └────┘ ┴ └
pid ─────┘ ┴ ┴ ┴ └────┘ ┴ └
st ───────────────────────────────────────────────────────
403 (l.map sigma.fst).disjoint ((bucket_array.as_list t).map sigma.fst),
id └───┘ └──────────────────┘ ┴ └───────┘
src ─────┘ └───┘┴ └─────────┘ └──────────────────┘┴ └────┘└───────┘└──
typ ─────┘ └───┘┴ └─────────┘ └──────────────────┘┴┴└────┘└───────┘└──
doc ─────┘ ┴ └─────────┘ └──────────────────┘┴ └────┘ └──
txt ─────┘ ┴ └─────────┘ ┴ └────┘ └──
par ─────┘ ┴ └─────────┘ ┴ └────┘ └──
pid ─────┘ ┴ └─────────┘ ┴ └────┘ └──
st ───────────────────────────────────────────────────────────────────────────
404 by simpa [list.nodup_append, not_or_distrib, and_comm, and.left_comm] using nd)
id └───────────────┘ └────────────┘ └──────┘ └───────────┘ └┘
src ──────┘└─────┘└───────────────┘└┘└────────────┘└┘└──────┘└┘└───────────┘└──────┘ └─
typ ──────┘└─────┘└───────────────┘└┘└────────────┘└┘└──────┘└┘└───────────┘└──────┘└┘└─
doc ──────┘└─────┘ └┘ └┘ └┘ └──────┘ └─
txt ──────┘└─────┘ └┘ └┘ └┘ └──────┘ └─
par ──────┘└─────┘ └┘ └┘ └┘ └──────┘ └─
pid ─────────────┘ └┘ └┘ └┘ └──────┘ └─
st ─────┘└──────────────────────────────────────────────────────────────────────────┘└─
405 with ⟨nd1, nd2, nm1, nm2, dj⟩,
src ────────────────────────────────┘
typ ────────────────────────────────┘
doc ────────────────────────────────┘
txt ────────────────────────────────┘
par ────────────────────────────────┘
pid ────────────────────────────────┘
st ────────────────────────────────┘└─
406 have v' := v.insert _ _ c.2 (λHc, nm2 $ (v.contains_aux_iff _ c.1).1 Hc),
id └──────┘ └─┘ └────────────────┘ ┴
src └─────────┘└──────┘└───┘ └─┘ └──┘ ┴ ┴ └────────────────┘└─┘ └────┘ ┴
typ └─────────┘└──────┘└───┘ └─┘ └──┘└─┘┴ ┴ └────────────────┘└─┘┴└────┘ ┴
doc └─────────┘ └───┘ └─┘ └──┘ ┴ ┴ └─┘ └────┘ ┴
txt └─────────┘ └───┘ └─┘ └──┘ ┴ ┴ └─┘ └────┘ ┴
par └─────────┘ └───┘ └─┘ └──┘ ┴ ┴ └─┘ └────┘ ┴
pid └─────┘┴└─┘ └───┘ └─┘ └──┘ ┴ ┴ └─┘ └────┘ ┴
st ─────────────────────────────────────────────────────────────────────────┘└─
407 apply IH _ _ v',
id └┘ └┘
src └────┘ └───┘
typ └────┘└┘└───┘└┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ └───┘
st ────────────────┘└─
408 suffices : ∀ ⦃a : α⦄ (b : β a), sigma.mk a b ∈ l →
id ┴ ┴ ┴
src └─────────┘ └────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
typ └─────────┘ └────┘┴└─────┘ ┴ ┴ ┴ ┴ ┴ ┴┴┴┴┴ └
doc └─────────┘ └────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
txt └─────────┘ └────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
par └─────────┘ └────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
pid └───────┘└┘ └────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
st ─────────────────────────────────────────────────────
409 ∀ (b' : β a), sigma.mk a b' ∈ (reinsert_aux hash_fn t c.1 c.2).as_list → false,
id ┴ └──────┘ ┴ └──────────┘ └─────┘ ┴ ┴ └───┘
src ───┘ └─────┘ ┴ ┴ ┴└──────┘┴ ┴ ┴ ┴ └──────────┘┴ ┴ ┴ └─┘ └──────────┘ ┴└───┘
typ ───┘ └─────┘┴┴ ┴ ┴└──────┘┴ ┴ ┴┴┴ └──────────┘┴└─────┘┴┴┴ └─┘┴└──────────┘ ┴└───┘
doc ───┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘┴ ┴ ┴ └─┘ └──────────┘ ┴
txt ───┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────────┘ ┴
par ───┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────────┘ ┴
pid ───┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────────┘ ┴
st ─────────────────────────────────────────────────────────────────────────────────┘└─
410 { simpa [list.nodup_append, nd1, v'.as_list_nodup _, list.disjoint] },
id └───────────────┘ └─┘ └──────────────┘ └───────────┘
src └─────┘└───────────────┘└┘ └┘└──────────────┘└──┘└───────────┘└┘
typ └─────┘└───────────────┘└┘└─┘└┘└──────────────┘└──┘└───────────┘└┘
doc └─────┘ └┘ └┘ └──┘└───────────┘└┘
txt └─────┘ └┘ └┘ └──┘ └┘
par └─────┘ └┘ └┘ └──┘ └┘
pid ┴┴ └┘ └┘ └──┘ ┴┴
st ───┘└────────────────────────────────────────────────────────────────┘└┘└
411 intros a b m1 b' m2,
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └───────────┘
st ────────────────────┘└─
412 rcases (reinsert_aux hash_fn t c.1 c.2).mem_as_list.1 m2 with ⟨i, im⟩,
id └──────────┘ └─────┘ ┴ ┴ └┘
src └─────┘ └──────────┘┴ ┴ ┴ └─┘ └────────────────┘ └───────────┘
typ └─────┘ └──────────┘┴└─────┘┴┴┴ └─┘┴└────────────────┘└┘└───────────┘
doc └─────┘ └──────────┘┴ ┴ ┴ └─┘ └────────────────┘ └───────────┘
txt └─────┘ ┴ ┴ ┴ └─┘ └────────────────┘ └───────────┘
par └─────┘ ┴ ┴ ┴ └─┘ └────────────────┘ └───────────┘
pid ┴ ┴ ┴ ┴ └─┘ └────────────────┘ └───────────┘
st ──────────────────────────────────────────────────────────────────────┘└─
413 have : sigma.mk a b' ∉ array.read t i,
id └──────┘ ┴ └┘ └────────┘ ┴ ┴
src └─────┘└──────┘┴ ┴ ┴ ┴└────────┘┴ ┴
typ └─────┘└──────┘┴┴┴└┘┴ ┴└────────┘┴┴┴┴
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────┘└─
414 { intro m3,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └─┘
st ───┘└──────┘└─
415 have : a ∈ list.map sigma.fst t.as_list :=
id ┴ └──────┘ └───────┘ └───────┘
src └─────┘ ┴ ┴└──────┘┴└───────┘┴└───────┘└───
typ └─────┘┴┴ ┴└──────┘┴└───────┘┴└───────┘└───
doc └─────┘ ┴ ┴ ┴ ┴└───────┘└───
txt └─────┘ ┴ ┴ ┴ ┴ └───
par └─────┘ ┴ ┴ ┴ ┴ └───
pid └───┘└┘ ┴ ┴ ┴ ┴ └───
st ───────────────────────────────────────────────
416 list.mem_map_of_mem sigma.fst (t.mem_as_list.2 ⟨_, m3⟩),
id └─────────────────┘ └───────┘ └───────────┘ └┘
src ─────┘└─────────────────┘┴└───────┘┴ └───────────┘└─┘ └─┘ └┘
typ ─────┘└─────────────────┘┴└───────┘┴ └───────────┘└─┘ └─┘└┘└┘
doc ─────┘ ┴ ┴ └─┘ └─┘ └┘
txt ─────┘ ┴ ┴ └─┘ └─┘ └┘
par ─────┘ ┴ ┴ └─┘ └─┘ └┘
pid ─────┘ ┴ ┴ └─┘ └─┘ └┘
st ────────────────────────────────────────────────────────────┘└─
417 exact dj (list.mem_map_of_mem sigma.fst m1) this },
id └┘ └─────────────────┘ └───────┘ └┘ └──┘
src └────┘ ┴ └─────────────────┘┴└───────┘┴ └┘ ┴
typ └────┘└┘┴ └─────────────────┘┴└───────┘┴└┘└┘└──┘┴
doc └────┘ ┴ ┴ ┴ └┘ ┴
txt └────┘ ┴ ┴ ┴ └┘ ┴
par └────┘ ┴ ┴ ┴ └┘ ┴
pid ┴ ┴ ┴ ┴ └┘ ┴
st ────────────────────────────────────────────────────┘└┘└
418 by_cases h : mk_idx n' (hash_fn c.1) = i,
id └────┘ └┘ └─────┘ ┴ ┴
src └───────┘ └─┘└────┘┴ ┴ ┴ └──┘ ┴
typ └───────┘ └─┘└────┘┴└┘┴ └─────┘┴┴└──┘ ┴┴
doc └───────┘ └─┘└────┘┴ ┴ ┴ └──┘ ┴
txt └───────┘ └─┘ ┴ ┴ ┴ └──┘ ┴
par └───────┘ └─┘ ┴ ┴ ┴ └──┘ ┴
pid ┴ └─┘ ┴ ┴ ┴ └──┘ ┴
st ─────────────────────────────────────────┘└─
419 { subst h,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───┘└─────┘└─
420 have e : sigma.mk a b' = ⟨c.1, c.2⟩,
id └──────┘ ┴ └┘ ┴
src └───────┘└──────┘┴ ┴ ┴ ┴ └──┘ └─┘
typ └───────┘└──────┘┴┴┴└┘┴ ┴ └──┘┴└─┘
doc └───────┘ ┴ ┴ ┴ ┴ └──┘ └─┘
txt └───────┘ ┴ ┴ ┴ ┴ └──┘ └─┘
par └───────┘ ┴ ┴ ┴ ┴ └──┘ └─┘
pid └────┘└─┘ ┴ ┴ ┴ ┴ └──┘ └─┘
st ──────────────────────────────────────┘└─
421 { simpa [reinsert_aux, bucket_array.modify, array.read_write, this] using im },
id └──────────┘ └─────────────────┘ └──────────────┘ └──┘ └┘
src └─────┘└──────────┘└┘└─────────────────┘└┘└──────────────┘└┘ └──────┘ ┴
typ └─────┘└──────────┘└┘└─────────────────┘└┘└──────────────┘└┘└──┘└──────┘└┘┴
doc └─────┘└──────────┘└┘└─────────────────┘└┘ └┘ └──────┘ ┴
txt └─────┘ └┘ └┘ └┘ └──────┘ ┴
par └─────┘ └┘ └┘ └┘ └──────┘ ┴
pid ┴┴ └┘ └┘ └┘ ┴┴└────┘ ┴
st ─────┘└─────────────────────────────────────────────────────────────────────────┘└┘└
422 injection e with e, subst a,
id ┴ ┴
src └────────┘ └─────┘ └────┘
typ └────────┘┴└─────┘ └────┘┴
doc └────────┘ └─────┘ └────┘
txt └────────┘ └─────┘ └────┘
par └────────┘ └─────┘ └────┘
pid ┴ └─────┘ ┴
st ─────────────────────┘└───────┘└─
423 exact nm1.elim (@list.mem_map_of_mem _ _ sigma.fst _ _ m1) },
id └──────┘ └─────────────────┘ └───────┘ └┘
src └────┘└──────┘┴ └─────────────────┘└───┘└───────┘└───┘ └┘
typ └────┘└──────┘┴ └─────────────────┘└───┘└───────┘└───┘└┘└┘
doc └────┘ ┴ └───┘ └───┘ └┘
txt └────┘ ┴ └───┘ └───┘ └┘
par └────┘ ┴ └───┘ └───┘ └┘
pid ┴ ┴ └───┘ └───┘ ┴┴
st ──────────────────────────────────────────────────────────────┘└┘└
424 { apply this,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────┘└─
425 simpa [reinsert_aux, bucket_array.modify, array.read_write_of_ne _ _ h] using im }
id └──────────┘ └─────────────────┘ └────────────────────┘ ┴ └┘
src └─────┘└──────────┘└┘└─────────────────┘└┘└────────────────────┘└───┘ └──────┘ ┴
typ └─────┘└──────────┘└┘└─────────────────┘└┘└────────────────────┘└───┘┴└──────┘└┘┴
doc └─────┘└──────────┘└┘└─────────────────┘└┘ └───┘ └──────┘ ┴
txt └─────┘ └┘ └┘ └───┘ └──────┘ ┴
par └─────┘ └┘ └┘ └───┘ └──────┘ ┴
pid ┴┴ └┘ └┘ └───┘ ┴┴└────┘ ┴
st ────────────────────────────────────────────────────────────────────────────────────┘└─
426 end
st ──┘
427
428 /-- Insert a key-value pair into the map. (Modifies `m` in-place when applicable) -/
429 def insert : Π (m : hash_map α β) (a : α) (b : β a), hash_map α β
id ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴
src ┴ └──────┘ └──────┘
typ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴
doc └──────┘ └──────┘
430 | ⟨hash_fn, size, n, buckets, v⟩ a b :=
id └─────┘ └──┘ ┴ └─────┘ ┴ ┴ ┴
typ └─────┘ └──┘ ┴ └─────┘ ┴ ┴ ┴
431 let bkt := buckets.read hash_fn a in
id └─┘ └───┘
src └───┘
typ └─┘ └───┘
doc └───┘
432 if hc : contains_aux a bkt then
id └┘ └──────────┘ └─┘
src └┘ └──────────┘
typ └┘ └──────────┘ └─┘
doc └──────────┘
433 { hash_fn := hash_fn,
434 size := size,
435 nbuckets := n,
436 buckets := buckets.modify hash_fn a (replace_aux a b),
id └─────┘ └─────────┘
src └─────┘ └─────────┘
typ └─────┘ └─────────┘
doc └─────┘ └─────────┘
437 is_valid := v.replace _ a b hc }
id └──────┘ └┘
src └──────┘
typ └──────┘ └┘
438 else
439 let size' := size + 1,
id └─┘ └───┘ ┴
src ┴
typ └─┘ └───┘ ┴
440 buckets' := buckets.modify hash_fn a (λl, ⟨a, b⟩::l),
id └──────┘ └─────┘ ┴ └┘┴
src └─────┘ └┘
typ └──────┘ └─────┘ ┴ └┘┴
doc └─────┘
441 valid' := v.insert _ a b hc in
id └────┘ └─────┘ └┘
src └─────┘
typ └────┘ └─────┘ └┘
442 if size' ≤ n.1 then
id └───┘ ┴ ┴
src ┴ ┴
typ └───┘ ┴ ┴
443 { hash_fn := hash_fn,
444 size := size',
id └───┘
typ └───┘
445 nbuckets := n,
446 buckets := buckets',
id └──────┘
typ └──────┘
447 is_valid := valid' }
id └────┘
typ └────┘
448 else
449 let n' : ℕ+ := ⟨n.1 * 2, mul_pos n.2 dec_trivial⟩,
id └┘ ┴ ┴ └─────┘ ┴ └─────────┘
src └┘ ┴ ┴ └─────┘ ┴ └─────────┘
typ └┘ ┴ ┴ └─────┘ ┴ └─────────┘
doc └┘ └─────────┘
450 buckets'' : bucket_array α β n' :=
id └──────────┘ ┴ ┴ └┘
src └──────────┘
typ └──────────┘ ┴ ┴ └┘
doc └──────────┘
451 buckets'.foldl (mk_array _ []) (reinsert_aux hash_fn) in
id └──────┘└────┘ └──────┘ └┘ └──────────┘
src └────┘ └──────┘ └┘ └──────────┘
typ └──────┘└────┘ └──────┘ └┘ └──────────┘
doc └────┘ └──────────┘
452 { hash_fn := hash_fn,
453 size := size',
id └───┘
typ └───┘
454 nbuckets := n',
id └┘
typ └┘
455 buckets := buckets'',
id └───────┘
typ └───────┘
456 is_valid := insert_lemma _ valid' }
id └──────────┘ └────┘
src └──────────┘
typ └──────────┘ └────┘
457
458 theorem mem_insert : Π (m : hash_map α β) (a b a' b'),
id ┴ └──────┘ ┴ ┴ ┴ ┴ └┘ └┘
src └──────┘
typ ┴ └──────┘ ┴ ┴ ┴ ┴ └┘ └┘
doc └──────┘
459 (sigma.mk a' b' : sigma β) ∈ (m.insert a b).entries ↔
id └──────┘ └┘ └┘ └───┘ ┴ ┴ ┴└─────┘ ┴ ┴ └─────┘ ┴
src └──────┘ └───┘ ┴ └─────┘ └─────┘ ┴
typ └──────┘ └┘ └┘ └───┘ ┴ ┴ ┴└─────┘ ┴ ┴ └─────┘ ┴
doc └─────┘ └─────┘
460 if a = a' then b == b' else sigma.mk a' b' ∈ m.entries
id ┴ ┴ └┘ ┴ └┘ └┘ └──────┘ └┘ └┘ ┴ ┴└──────┘
src ┴ └┘ └──────┘ ┴ └──────┘
typ ┴ ┴ └┘ ┴ └┘ └┘ └──────┘ └┘ └┘ ┴ ┴└──────┘
doc └──────┘
461 | ⟨hash_fn, size, n, bkts, v⟩ a b a' b' := begin
st └─────
462 let bkt := bkts.read hash_fn a,
id └───────┘ └─────┘ ┴
src └─────────┘└───────┘┴ ┴
typ └─────────┘└───────┘┴└─────┘┴┴
doc └─────────┘└───────┘┴ ┴
txt └─────────┘ ┴ ┴
par └─────────┘ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴
st ───────────────────────────────┘└─
463 have nd : (bkt.map sigma.fst).nodup := v.nodup (mk_idx n (hash_fn a)),
id └─────┘ └───────┘ └─────┘ └────┘ ┴ └─────┘ ┴
src └────────┘ └─────┘┴└───────┘└─────────┘└─────┘┴ └────┘┴ ┴ ┴ └┘
typ └────────┘ └─────┘┴└───────┘└─────────┘└─────┘┴ └────┘┴┴┴ └─────┘┴┴└┘
doc └────────┘ ┴ └─────────┘ ┴ └────┘┴ ┴ ┴ └┘
txt └────────┘ ┴ └─────────┘ ┴ ┴ ┴ ┴ └┘
par └────────┘ ┴ └─────────┘ ┴ ┴ ┴ ┴ └┘
pid └─────┘└─┘ ┴ └────┘└───┘ ┴ ┴ ┴ ┴ └┘
st ──────────────────────────────────────────────────────────────────────┘└─
464 have lem : Π (bkts' : bucket_array α β n) (v1 u w)
id └──────────┘ ┴ ┴ ┴
src └─────────┘ └────────┘└──────────┘┴ ┴ ┴ └──────────
typ └─────────┘ └────────┘└──────────┘┴┴┴┴┴┴└──────────
doc └─────────┘ └────────┘└──────────┘┴ ┴ ┴ └──────────
txt └─────────┘ └────────┘ ┴ ┴ ┴ └──────────
par └─────────┘ └────────┘ ┴ ┴ ┴ └──────────
pid └──────┘└─┘ └────────┘ ┴ ┴ ┴ └──────────
st ─────────────────────────────────────────────────────
465 (hl : bucket_array.as_list bkts = u ++ v1 ++ w)
id ┴ └┘
src ─────────┘ ┴ ┴┴┴ ┴└┘┴ ┴ ┴ └─
typ ─────────┘ ┴ ┴┴┴ ┴└┘┴ ┴ ┴ └─
doc ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
txt ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
par ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
pid ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
st ────────────────────────────────────────────────────
466 (hfl : bucket_array.as_list bkts' = u ++ [⟨a, b⟩] ++ w)
id └──────────────────┘ ┴
src ──────────┘└──────────────────┘┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─
typ ──────────┘└──────────────────┘┴ ┴┴┴ ┴ ┴ └┘ ┴ ┴ ┴ └─
doc ──────────┘└──────────────────┘┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─
txt ──────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─
par ──────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─
pid ──────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─
st ────────────────────────────────────────────────────────────
467 (veq : (v1 = [] ∧ ¬ contains_aux a bkt) ∨ ∃b'', v1 = [⟨a, b''⟩]),
id ┴ ┴ └──────────┘ └─┘ ┴ ┴ ┴ ┴ ┴
src ──────────┘ ┴ ┴ ┴┴┴┴┴└──────────┘┴ ┴ └┘┴┴┴└─┘┴┴ ┴ ┴┴ └┘ ┴┴┴ └
typ ──────────┘ ┴ ┴ ┴┴┴┴┴└──────────┘┴ ┴└─┘└┘┴┴┴└─┘┴┴ ┴ ┴┴ └┘ ┴┴┴ └
doc ──────────┘ ┴ ┴ ┴ ┴ ┴└──────────┘┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └
txt ──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └
par ──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └
pid ──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └
st ──────────────────────────────────────────────────────────────────────
468 sigma.mk a' b' ∈ bkts'.as_list ↔
id ┴ └──────┘
src ───┘ ┴ ┴ ┴┴┴ └──────┘┴ └
typ ───┘ ┴ ┴ ┴┴┴ └──────┘┴ └
doc ───┘ ┴ ┴ ┴ ┴ └──────┘┴ └
txt ───┘ ┴ ┴ ┴ ┴ ┴ └
par ───┘ ┴ ┴ ┴ ┴ ┴ └
pid ───┘ ┴ ┴ ┴ ┴ ┴ └
st ─────────────────────────────────────
469 if a = a' then b == b' else sigma.mk a' b' ∈ bkts.as_list,
id ┴ └┘ └──────┘ └┘ └┘ └──────────┘
src ───┘ └─┘ ┴ └────┘ ┴└┘┴ └────┘└──────┘┴ ┴ ┴ ┴└──────────┘
typ ───┘ └─┘ ┴ └────┘┴┴└┘┴ └────┘└──────┘┴└┘┴└┘┴ ┴└──────────┘
doc ───┘ └─┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴└──────────┘
txt ───┘ └─┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
par ───┘ └─┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
pid ───┘ └─┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────┘└─
470 { intros bkts' v1 u w hl hfl veq,
src └────────────────────────────┘
typ └────────────────────────────┘
doc └────────────────────────────┘
txt └────────────────────────────┘
par └────────────────────────────┘
pid └──────────────────────┘
st ───┘└────────────────────────────┘└─
471 rw [hl, hfl],
id └┘ └─┘
src └──┘ └┘ ┴
typ └──┘└┘└┘└─┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ─────────┘└───┘└──
472 by_cases h : a = a',
id ┴ └┘
src └───────┘ └─┘ ┴ ┴
typ └───────┘ └─┘┴┴ ┴└┘
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ──────────────────────┘└─
473 { subst a',
id └┘
src └────┘
typ └────┘└┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────┘└──────┘└─
474 suffices : b = b' ∨ sigma.mk a b' ∈ u ∨ sigma.mk a b' ∈ w ↔ b = b',
id ┴ └──────┘ ┴ ┴ ┴ └┘
src └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴└──────┘┴┴┴ ┴ ┴┴┴ ┴┴┴ ┴└┘
doc └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───────┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────┘└─
475 { simpa [eq_comm, or.left_comm] },
id └─────┘ └──────────┘
src └─────┘└─────┘└┘└──────────┘└┘
typ └─────┘└─────┘└┘└──────────┘└┘
doc └─────┘ └┘ └┘
txt └─────┘ └┘ └┘
par └─────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ───────┘└────────────────────────────┘└┘└
476 refine or_iff_left_of_imp (not.elim $ not_or_distrib.2 _),
id └────────────────┘ └──────┘ └────────────┘
src └─────┘└────────────────┘┴ └──────┘┴ ┴└────────────┘└───┘
typ └─────┘└────────────────┘┴ └──────┘┴ ┴└────────────┘└───┘
doc └─────┘ ┴ ┴ ┴ └───┘
txt └─────┘ ┴ ┴ ┴ └───┘
par └─────┘ ┴ ┴ ┴ └───┘
pid ┴ ┴ ┴ ┴ └───┘
st ──────────────────────────────────────────────────────────────┘└─
477 rcases veq with ⟨rfl, Hnc⟩ | ⟨b'', rfl⟩,
id └─┘
src └─────┘ └───────────────────────────┘
typ └─────┘└─┘└───────────────────────────┘
doc └─────┘ └───────────────────────────┘
txt └─────┘ └───────────────────────────┘
par └─────┘ └───────────────────────────┘
pid ┴ └───────────────────────────┘
st ────────────────────────────────────────────┘└─
478 { have na := (not_iff_not_of_iff $ v.contains_aux_iff _ _).1 Hnc,
id └────────────────┘ └────────────────┘ └─┘
src └─────────┘ └────────────────┘┴ ┴└────────────────┘└──────┘
typ └─────────┘ └────────────────┘┴ ┴└────────────────┘└──────┘└─┘
doc └─────────┘ ┴ ┴ └──────┘
txt └─────────┘ ┴ ┴ └──────┘
par └─────────┘ ┴ ┴ └──────┘
pid └─────┘┴└─┘ ┴ ┴ └──────┘
st ───────┘└────────────────────────────────────────────────────────────┘└─
479 simp [hl, not_or_distrib] at na, simp [na] },
id └┘ └────────────┘ └┘
src └────┘ └┘└────────────┘└─────┘ └────┘ └┘
typ └────┘└┘└┘└────────────┘└─────┘ └────┘└┘└┘
doc └────┘ └┘ └─────┘ └────┘ └┘
txt └────┘ └┘ └─────┘ └────┘ └┘
par └────┘ └┘ └─────┘ └────┘ └┘
pid ┴┴ └┘ ┴┴└───┘ ┴┴ ┴┴
st ──────────────────────────────────────┘└──────────┘└┘└
480 { have nd' := v.as_list_nodup _,
id └─────────────┘
src └──────────┘└─────────────┘└┘
typ └──────────┘└─────────────┘└┘
doc └──────────┘ └┘
txt └──────────┘ └┘
par └──────────┘ └┘
pid └──────┘┴└─┘ └┘
st ────────────────────────────────────┘└─
481 simp [hl, list.nodup_append] at nd', simp [nd'] } },
id └┘ └───────────────┘ └─┘
src └────┘ └┘└───────────────┘└──────┘ └────┘ └┘
typ └────┘└┘└┘└───────────────┘└──────┘ └────┘└─┘└┘
doc └────┘ └┘ └──────┘ └────┘ └┘
txt └────┘ └┘ └──────┘ └────┘ └┘
par └────┘ └┘ └──────┘ └────┘ └┘
pid ┴┴ └┘ ┴┴└────┘ ┴┴ ┴┴
st ──────────────────────────────────────────┘└───────────┘└──┘└
482 { suffices : sigma.mk a' b' ∉ v1, {simp [h, ne.symm h, this]},
id └──────┘ └┘ └┘ └┘ ┴ └─────┘ ┴ └──┘
src └─────────┘└──────┘┴ ┴ ┴ ┴ └────┘ └┘└─────┘┴ └┘ ┴
typ └─────────┘└──────┘┴└┘┴└┘┴ ┴└┘ └────┘┴└┘└─────┘┴┴└┘└──┘┴
doc └─────────┘ ┴ ┴ ┴ ┴ └────┘ └┘ ┴ └┘ ┴
txt └─────────┘ ┴ ┴ ┴ ┴ └────┘ └┘ ┴ └┘ ┴
par └─────────┘ ┴ ┴ ┴ ┴ └────┘ └┘ ┴ └┘ ┴
pid └───────┘└┘ ┴ ┴ ┴ ┴ ┴┴ └┘ ┴ └┘ ┴
st ───────────────────────────────────┘└──────────────────────────┘└┘└
483 rcases veq with ⟨rfl, Hnc⟩ | ⟨b'', rfl⟩; simp [ne.symm h] } },
id └─┘ └─────┘ ┴
src └─────┘ └───────────────────────────┘ └────┘└─────┘┴ └┘
typ └─────┘└─┘└───────────────────────────┘ └────┘└─────┘┴┴└┘
doc └─────┘ └───────────────────────────┘ └────┘ ┴ └┘
txt └─────┘ └───────────────────────────┘ └────┘ ┴ └┘
par └─────┘ └───────────────────────────┘ └────┘ ┴ └┘
pid ┴ └───────────────────────────┘ ┴┴ ┴ ┴┴
st ───────────────────────────────────────────────────────────────┘└──┘└
484 by_cases Hc : (contains_aux a bkt : Prop),
id └──────────┘ ┴ └─┘
src └───────┘ └─┘ └──────────┘┴ ┴ └─┘ ┴
typ └───────┘ └─┘ └──────────┘┴┴┴└─┘└─┘ ┴
doc └───────┘ └─┘ └──────────┘┴ ┴ └─┘ ┴
txt └───────┘ └─┘ ┴ ┴ └─┘ ┴
par └───────┘ └─┘ ┴ ┴ └─┘ ┴
pid ┴ └─┘ ┴ ┴ └─┘ ┴
st ──────────────────────────────────────────┘└─
485 { rcases hash_map.valid.replace_aux a b (array.read bkts (mk_idx n (hash_fn a)))
id └────────────────────────┘ ┴ └────────┘ └──┘ └────┘ ┴ └─────┘ ┴
src └─────┘└────────────────────────┘┴ ┴ ┴ └────────┘┴ ┴ └────┘┴ ┴ ┴ └───
typ └─────┘└────────────────────────┘┴ ┴┴┴ └────────┘┴└──┘┴ └────┘┴┴┴ └─────┘┴┴└───
doc └─────┘ ┴ ┴ ┴ ┴ ┴ └────┘┴ ┴ ┴ └───
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
st ───┘└──────────────────────────────────────────────────────────────────────────────
486 ((contains_aux_iff nd).1 Hc) with ⟨u', w', b'', hl', hfl'⟩,
id └──────────────┘ └┘ └┘
src ─────┘ └──────────────┘┴ └──┘ └─────────────────────────────┘
typ ─────┘ └──────────────┘┴└┘└──┘└┘└─────────────────────────────┘
doc ─────┘ ┴ └──┘ └─────────────────────────────┘
txt ─────┘ ┴ └──┘ └─────────────────────────────┘
par ─────┘ ┴ └──┘ └─────────────────────────────┘
pid ─────┘ ┴ └──┘ └─────────────────────────────┘
st ───────────────────────────────────────────────────────────────┘└─
487 rcases (append_of_modify u' [⟨a, b''⟩] [⟨a, b⟩] w' hl' hfl') with ⟨u, w, hl, hfl⟩,
id └──────────────┘ └┘ └─┘ ┴ ┴ ┴ ┴ └┘ └─┘ └──┘
src └─────┘ └──────────────┘┴ ┴ └┘ ┴ ┴┴ └┘ ┴┴┴ ┴ ┴ └────────────────────┘
typ └─────┘ └──────────────┘┴└┘┴ └┘└─┘┴ ┴┴ ┴└┘┴┴┴┴└┘┴└─┘┴└──┘└────────────────────┘
doc └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────────────────────┘
txt └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────────────────────┘
par └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────────────────────┘
pid ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────────────────────┘
st ────────────────────────────────────────────────────────────────────────────────────┘└─
488 simpa [insert, @dif_pos (contains_aux a bkt) _ Hc]
id └────┘ └─────┘ └──────────┘ ┴ └─┘ └┘
src └─────┘└────┘└┘ └─────┘┴ └──────────┘┴ ┴ └──┘ └─
typ └─────┘└────┘└┘ └─────┘┴ └──────────┘┴┴┴└─┘└──┘└┘└─
doc └─────┘└────┘└┘ ┴ └──────────┘┴ ┴ └──┘ └─
txt └─────┘ └┘ ┴ ┴ ┴ └──┘ └─
par └─────┘ └┘ ┴ ┴ ┴ └──┘ └─
pid ┴┴ └┘ ┴ ┴ ┴ └──┘ ┴└
st ───────────────────────────────────────────────────────
489 using lem _ _ u w hl hfl (or.inr ⟨b'', rfl⟩) },
id └─┘ ┴ ┴ └┘ └─┘ └────┘ └─┘ └─┘
src ───────────┘ └───┘ ┴ ┴ ┴ ┴ └────┘┴ └┘└─┘└─┘
typ ───────────┘└─┘└───┘┴┴┴┴└┘┴└─┘┴ └────┘┴ └─┘└┘└─┘└─┘
doc ───────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ └┘ └─┘
txt ───────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ └┘ └─┘
par ───────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ └┘ └─┘
pid ─────┘└────┘ └───┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘┴
st ──────────────────────────────────────────────────┘└┘└
490 { let size' := size + 1,
id └──┘ ┴
src └───────────┘ ┴┴└┘
typ └───────────┘└──┘┴┴└┘
doc └───────────┘ ┴ └┘
txt └───────────┘ ┴ └┘
par └───────────┘ ┴ └┘
pid └───────┘┴└─┘ ┴ ┴┴
st ────────────────────────┘└─
491 let bkts' := bkts.modify hash_fn a (λl, ⟨a, b⟩::l),
id └─────────┘ └─────┘ ┴ ┴
src └───────────┘└─────────┘┴ ┴ ┴ └─┘ └┘ ┴ ┴
typ └───────────┘└─────────┘┴└─────┘┴ ┴ └─┘ ┴└┘┴┴ ┴
doc └───────────┘└─────────┘┴ ┴ ┴ └─┘ └┘ ┴ ┴
txt └───────────┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴
par └───────────┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴
pid └───────┘┴└─┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴
st ─────────────────────────────────────────────────────┘└─
492 have mi : sigma.mk a' b' ∈ bkts'.as_list ↔
id └───────────┘
src └────────┘ ┴ ┴ ┴ ┴└───────────┘┴ └
typ └────────┘ ┴ ┴ ┴ ┴└───────────┘┴ └
doc └────────┘ ┴ ┴ ┴ ┴└───────────┘┴ └
txt └────────┘ ┴ ┴ ┴ ┴ ┴ └
par └────────┘ ┴ ┴ ┴ ┴ ┴ └
pid └─────┘└─┘ ┴ ┴ ┴ ┴ ┴ └
st ───────────────────────────────────────────────
493 if a = a' then b == b' else sigma.mk a' b' ∈ bkts.as_list :=
id ┴ └──────┘ └┘ └┘ └──────────┘
src ───────┘ └─┘ ┴ └────┘ ┴ ┴ └────┘└──────┘┴ ┴ ┴ ┴└──────────┘└───
typ ───────┘ └─┘ ┴ └────┘┴┴ ┴ └────┘└──────┘┴└┘┴└┘┴ ┴└──────────┘└───
doc ───────┘ └─┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴└──────────┘└───
txt ───────┘ └─┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └───
par ───────┘ └─┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └───
pid ───────┘ └─┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └───
st ─────────────────────────────────────────────────────────────────────
494 let ⟨u, w, hl, hfl⟩ := append_of_modify [] [] [⟨a, b⟩] _ rfl rfl in
id ┴ ┴ └┘ └─┘ └──────────────┘ ┴ ┴ └─┘
src ─────┘ ┴ └┘ └┘ └┘ └───┘└──────────────┘┴ ┴ ┴ └┘ ┴ └─┘ ┴└─┘└───
typ ─────┘ ┴ ┴└┘┴└┘└┘└┘└─┘└───┘└──────────────┘┴ ┴ ┴ ┴└┘┴┴ └─┘ ┴└─┘└───
doc ─────┘ ┴ └┘ └┘ └┘ └───┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ └───
txt ─────┘ ┴ └┘ └┘ └┘ └───┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ └───
par ─────┘ ┴ └┘ └┘ └┘ └───┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ └───
pid ─────┘ ┴ └┘ └┘ └┘ └───┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ └───
st ──────────────────────────────────────────────────────────────────────────
495 lem bkts' _ u w hl hfl $ or.inl ⟨rfl, Hc⟩,
id └─┘ └───┘ └────┘ └┘
src ─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴└────┘┴ └┘ ┴
typ ─────┘└─┘┴└───┘└─┘ ┴ ┴ ┴ ┴ ┴└────┘┴ └┘└┘┴
doc ─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
txt ─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
par ─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
pid ─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
st ──────────────────────────────────────────────┘└─
496 simp [insert, @dif_neg (contains_aux a bkt) _ Hc],
id └────┘ └─────┘ └──────────┘ ┴ └─┘ └┘
src └────┘└────┘└┘ └─────┘┴ └──────────┘┴ ┴ └──┘ ┴
typ └────┘└────┘└┘ └─────┘┴ └──────────┘┴┴┴└─┘└──┘└┘┴
doc └────┘└────┘└┘ ┴ └──────────┘┴ ┴ └──┘ ┴
txt └────┘ └┘ ┴ ┴ ┴ └──┘ ┴
par └────┘ └┘ ┴ ┴ ┴ └──┘ ┴
pid ┴┴ └┘ ┴ ┴ ┴ └──┘ ┴
st ────────────────────────────────────────────────────┘└─
497 by_cases h : size' ≤ n.1,
id └───┘ ┴ ┴
src └───────┘ └─┘ ┴┴┴ └┘
typ └───────┘ └─┘└───┘┴┴┴┴└┘
doc └───────┘ └─┘ ┴ ┴ └┘
txt └───────┘ └─┘ ┴ ┴ └┘
par └───────┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ └┘
st ───────────────────────────┘└─
498 -- TODO(Mario): Why does the by_cases assumption look different than the stated one?
st ─────────────────────────────────────────────────────────────────────────────────────────
499 { simpa [show size' ≤ n.1, from h] using mi },
id └───┘ ┴ ┴ └┘
src └─────┘ ┴ ┴ ┴ └───────┘ └──────┘ ┴
typ └─────┘ ┴└───┘┴ ┴┴└───────┘┴└──────┘└┘┴
doc └─────┘ ┴ ┴ ┴ └───────┘ └──────┘ ┴
txt └─────┘ ┴ ┴ ┴ └───────┘ └──────┘ ┴
par └─────┘ ┴ ┴ ┴ └───────┘ └──────┘ ┴
pid ┴┴ ┴ ┴ ┴ └───────┘ ┴┴└────┘ ┴
st ─────┘└────────────────────────────────────────┘└┘└
500 { let n' : ℕ+ := ⟨n.1 * 2, mul_pos n.2 dec_trivial⟩,
id └┘ ┴ └─────┘ ┴ └─────────┘
src └───────┘└┘└──┘ └─┘┴└──┘└─────┘┴ └─┘└─────────┘┴
typ └───────┘└┘└──┘ └─┘┴└──┘└─────┘┴┴└─┘└─────────┘┴
doc └───────┘└┘└──┘ └─┘ └──┘ ┴ └─┘└─────────┘┴
txt └───────┘ └──┘ └─┘ └──┘ ┴ └─┘ ┴
par └───────┘ └──┘ └─┘ └──┘ ┴ └─┘ ┴
pid └────┘└─┘ └──┘ └─┘ └──┘ ┴ └─┘ ┴
st ──────────────────────────────────────────────────────┘└─
501 let bkts'' : bucket_array α β n' := bkts'.foldl (mk_array _ []) (reinsert_aux hash_fn),
id └──────────┘ ┴ ┴ └┘ └─────────┘ └──────┘ └──────────┘ └─────┘
src └───────────┘└──────────┘┴ ┴ ┴ └──┘└─────────┘┴ └──────┘└─┘ └┘ └──────────┘┴ ┴
typ └───────────┘└──────────┘┴┴┴┴┴└┘└──┘└─────────┘┴ └──────┘└─┘ └┘ └──────────┘┴└─────┘┴
doc └───────────┘└──────────┘┴ ┴ ┴ └──┘└─────────┘┴ └─┘ └┘ └──────────┘┴ ┴
txt └───────────┘ ┴ ┴ ┴ └──┘ ┴ └─┘ └┘ ┴ ┴
par └───────────┘ ┴ ┴ ┴ └──┘ ┴ └─┘ └┘ ┴ ┴
pid └────────┘└─┘ ┴ ┴ ┴ └──┘ ┴ └─┘ └┘ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────────────────────┘└─
502 suffices : sigma.mk a' b' ∈ bkts''.as_list ↔ sigma.mk a' b' ∈ bkts'.as_list.reverse,
id └────────────┘ └──────┘ └┘ └┘ └───────────────────┘
src └─────────┘ ┴ ┴ ┴ ┴└────────────┘┴ ┴└──────┘┴ ┴ ┴ ┴└───────────────────┘
typ └─────────┘ ┴ ┴ ┴ ┴└────────────┘┴ ┴└──────┘┴└┘┴└┘┴ ┴└───────────────────┘
doc └─────────┘ ┴ ┴ ┴ ┴└────────────┘┴ ┴ ┴ ┴ ┴ ┴└───────────────────┘
txt └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───────┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────────────┘└─
503 { simpa [show ¬ size' ≤ n.1, from h, mi] },
id ┴ └───┘ ┴ ┴ └┘
src └─────┘ ┴ ┴ ┴ ┴ └───────┘ └┘ └┘
typ └─────┘ ┴┴┴└───┘┴ ┴┴└───────┘┴└┘└┘└┘
doc └─────┘ ┴ ┴ ┴ ┴ └───────┘ └┘ └┘
txt └─────┘ ┴ ┴ ┴ ┴ └───────┘ └┘ └┘
par └─────┘ ┴ ┴ ┴ ┴ └───────┘ └┘ └┘
pid ┴┴ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴┴
st ───────┘└─────────────────────────────────────┘└┘└
504 rw [show bkts'' = bkts'.as_list.foldl _ _, from bkts'.foldl_eq _ _,
id └────┘ ┴ └─────────────────┘ └────────────┘
src └──┘ ┴ ┴ ┴└─────────────────┘└─────────┘└────────────┘└─────
typ └──┘ ┴└────┘┴┴┴└─────────────────┘└─────────┘└────────────┘└─────
doc └──┘ ┴ ┴ ┴└─────────────────┘└─────────┘ └─────
txt └──┘ ┴ ┴ ┴ └─────────┘ └─────
par └──┘ ┴ ┴ ┴ └─────────┘ └─────
pid └┘ ┴ ┴ ┴ └─────────┘ └─────
st ───────────────────────────────────────────────────────────────────────┘└─
505 ← list.foldr_reverse],
id └────────────────┘
src ───────────┘└────────────────┘┴
typ ───────────┘└────────────────┘┴
doc ───────────┘ ┴
txt ───────────┘ ┴
par ───────────┘ ┴
pid ───────────┘ ┴
st ─────────────────────────────┘└──
506 induction bkts'.as_list.reverse with a l IH,
id └───────────────────┘
src └────────┘└───────────────────┘└──────────┘
typ └────────┘└───────────────────┘└──────────┘
doc └────────┘└───────────────────┘└──────────┘
txt └────────┘ └──────────┘
par └────────┘ └──────────┘
pid ┴ ┴└─────────┘
st ────────────────────────────────────────────────┘└─
507 { simp [mk_as_list] },
id └────────┘
src └────┘└────────┘└┘
typ └────┘└────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ───────┘└────────────────┘└┘└
508 { cases a with a'' b'',
id ┴
src └────┘ └───────────┘
typ └────┘┴└───────────┘
doc └────┘ └───────────┘
txt └────┘ └───────────┘
par └────┘ └───────────┘
pid ┴ └───────────┘
st ───────────────────────────┘└─
509 let B := l.foldr (λ (y : sigma β) (x : bucket_array α β n'),
id └─────┘ └───┘ └──────────┘ ┴ ┴
src └───────┘└─────┘┴ └────┘└───┘┴ └─────┘└──────────┘┴ ┴ ┴ └──
typ └───────┘└─────┘┴ └────┘└───┘┴ └─────┘└──────────┘┴┴┴┴┴ └──
doc └───────┘ ┴ └────┘ ┴ └─────┘└──────────┘┴ ┴ ┴ └──
txt └───────┘ ┴ └────┘ ┴ └─────┘ ┴ ┴ ┴ └──
par └───────┘ ┴ └────┘ ┴ └─────┘ ┴ ┴ ┴ └──
pid └───┘┴└─┘ ┴ └────┘ ┴ └─────┘ ┴ ┴ ┴ └──
st ─────────────────────────────────────────────────────────────────────
510 reinsert_aux hash_fn x y.1 y.2) (mk_array n'.1 []),
id └──────────┘ └─────┘ └──────┘ └┘ └┘
src ─────────┘└──────────┘┴ ┴ ┴ └─┘ └──┘ └──────┘┴ └─┘└┘┴
typ ─────────┘└──────────┘┴└─────┘┴ ┴ └─┘ └──┘ └──────┘┴└┘└─┘└┘┴
doc ─────────┘└──────────┘┴ ┴ ┴ └─┘ └──┘ ┴ └─┘ ┴
txt ─────────┘ ┴ ┴ ┴ └─┘ └──┘ ┴ └─┘ ┴
par ─────────┘ ┴ ┴ ┴ └─┘ └──┘ ┴ └─┘ ┴
pid ─────────┘ ┴ ┴ ┴ └─┘ └──┘ ┴ └─┘ ┴
st ───────────────────────────────────────────────────────────┘└─
511 rcases append_of_modify [] [] [⟨a'', b''⟩] _ rfl rfl with ⟨u, w, hl, hfl⟩,
id └──────────────┘ ┴ └─┘ └─┘ ┴ └─┘
src └─────┘└──────────────┘┴ ┴ ┴┴ └┘ ┴┴└─┘ ┴└─┘└───────────────────┘
typ └─────┘└──────────────┘┴ ┴ ┴┴ └─┘└┘└─┘┴┴└─┘ ┴└─┘└───────────────────┘
doc └─────┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ └───────────────────┘
txt └─────┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ └───────────────────┘
par └─────┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ └───────────────────┘
pid ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ └───────────────────┘
st ────────────────────────────────────────────────────────────────────────────────┘└─
512 simp [IH.symm, or.left_comm, show B.as_list = _, from hl,
id └──────────┘ └───────┘ ┴ └┘
src └────┘ └┘└──────────┘└┘ ┴└───────┘┴ └───────┘ └─
typ └────┘└─────┘└┘└──────────┘└┘ ┴└───────┘┴┴└───────┘└┘└─
doc └────┘ └┘ └┘ ┴└───────┘┴ └───────┘ └─
txt └────┘ └┘ └┘ ┴ ┴ └───────┘ └─
par └────┘ └┘ └┘ ┴ ┴ └───────┘ └─
pid ┴┴ └┘ └┘ ┴ ┴ └───────┘ └─
st ──────────────────────────────────────────────────────────────────
513 show (reinsert_aux hash_fn B a'' b'').as_list = _, from hfl] } } }
id └──────────┘ └─────┘ ┴ └─┘ └─┘ ┴ └─┘
src ─────────────┘ ┴ └──────────┘┴ ┴ ┴ ┴ └────────┘ └───────┘ └┘
typ ─────────────┘ ┴ └──────────┘┴└─────┘┴┴┴└─┘┴└─┘└────────┘┴└───────┘└─┘└┘
doc ─────────────┘ ┴ └──────────┘┴ ┴ ┴ ┴ └────────┘ └───────┘ └┘
txt ─────────────┘ ┴ ┴ ┴ ┴ ┴ └────────┘ └───────┘ └┘
par ─────────────┘ ┴ ┴ ┴ ┴ ┴ └────────┘ └───────┘ └┘
pid ─────────────┘ ┴ ┴ ┴ ┴ ┴ └────────┘ └───────┘ ┴┴
st ──────────────────────────────────────────────────────────────────────────┘└─────
514 end
st ──┘
515
516 theorem find_insert_eq (m : hash_map α β) (a : α) (b : β a) : (m.insert a b).find a = some b :=
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴└─────┘ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src └──────┘ └─────┘ └──┘ ┴ └──┘
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴└─────┘ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
doc └──────┘ └─────┘ └──┘
517 (find_iff (m.insert a b) a b).2 $ (mem_insert m a b a b).2 $ by rw if_pos rfl
id └──────┘ ┴└─────┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └─┘
src └──────┘ └─────┘ ┴ └────────┘ ┴ └─┘└────┘┴└─┘└
typ └──────┘ ┴└─────┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└────┘┴└─┘└
doc └─────┘ └─┘ ┴ └
txt └─┘ ┴ └
par └─┘ ┴ └
pid ┴ ┴ └
st └──────────────
518
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
519 theorem find_insert_ne (m : hash_map α β) (a a' : α) (b : β a) (h : a ≠ a') :
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
src └──────┘ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
doc └──────┘
520 (m.insert a b).find a' = m.find a' :=
id ┴└─────┘ ┴ ┴ └──┘ └┘ ┴ ┴└───┘ └┘
src └─────┘ └──┘ ┴ └───┘
typ ┴└─────┘ ┴ ┴ └──┘ └┘ ┴ ┴└───┘ └┘
doc └─────┘ └──┘ └───┘
521 option.eq_of_eq_some $ λb',
id └──────────────────┘ └┘
src └──────────────────┘
typ └──────────────────┘ └┘
522 let t := mem_insert m a b a' b' in
id ┴ └────────┘ ┴ ┴ ┴ └┘ └┘
src └────────┘
typ ┴ └────────┘ ┴ ┴ ┴ └┘ └┘
523 (find_iff _ _ _).trans $ iff.trans (by rwa if_neg h at t) (find_iff _ _ _).symm
id └──────┘ └───┘ └───────┘ └────┘ ┴ └──────┘ └──┘
src └──────┘ └───┘ └───────┘ └──┘└────┘┴ └───┘ └──────┘ └──┘
typ └──────┘ └───┘ └───────┘ └──┘└────┘┴┴└───┘ └──────┘ └──┘
doc └──┘ ┴ └───┘
txt └──┘ ┴ └───┘
par └──┘ ┴ └───┘
pid ┴ ┴ └───┘
st └────────────────┘
524
525 theorem find_insert (m : hash_map α β) (a' a : α) (b : β a) :
id └──────┘ ┴ ┴ ┴ ┴ ┴
src └──────┘
typ └──────┘ ┴ ┴ ┴ ┴ ┴
doc └──────┘
526 (m.insert a b).find a' = if h : a = a' then some (eq.rec_on h b) else m.find a' :=
id ┴└─────┘ ┴ ┴ └──┘ └┘ ┴ └┘ ┴ ┴ └┘ └──┘ └───────┘ ┴ ┴ ┴└───┘ └┘
src └─────┘ └──┘ ┴ └┘ ┴ └──┘ └───────┘ └───┘
typ ┴└─────┘ ┴ ┴ └──┘ └┘ ┴ └┘ ┴ ┴ └┘ └──┘ └───────┘ ┴ ┴ ┴└───┘ └┘
doc └─────┘ └──┘ └───┘
527 if h : a = a' then by rw dif_pos h; exact
id └┘ ┴ ┴ └┘ └─────┘ ┴
src └┘ ┴ └─┘└─────┘┴ └─────
typ └┘ ┴ ┴ └┘ └─┘└─────┘┴┴ └─────
doc └─┘ ┴ └─────
txt └─┘ ┴ └─────
par └─┘ ┴ └─────
pid ┴ ┴ └
st └────────────────────
528 match a', h with ._, rfl := find_insert_eq m a b end
id └┘ ┴ └─┘ └────────────┘ ┴ ┴ ┴
src ─┘ ┴ └┘ └────┘ └┘└─┘└──┘└────────────┘┴ ┴ ┴ └───┘
typ ─┘ ┴└┘└┘┴└────┘ └┘└─┘└──┘└────────────┘┴┴┴┴┴┴└───┘
doc ─┘ ┴ └┘ └────┘ └┘ └──┘ ┴ ┴ ┴ └───┘
txt ─┘ ┴ └┘ └────┘ └┘ └──┘ ┴ ┴ ┴ └───┘
par ─┘ ┴ └┘ └────┘ └┘ └──┘ ┴ ┴ ┴ └───┘
pid ─┘ ┴ └┘ └────┘ └┘ └──┘ ┴ ┴ ┴ └──┘┴
st ──────────────────────────────────────────────────────┘
529 else by rw dif_neg h; exact find_insert_ne m a a' b h
id └─────┘ ┴ └────────────┘ ┴ ┴ └┘ ┴ ┴
src └─┘└─────┘┴ └────┘└────────────┘┴ ┴ ┴ ┴ ┴ └
typ └─┘└─────┘┴┴ └────┘└────────────┘┴┴┴┴┴└┘┴┴┴┴└
doc └─┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └
txt └─┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └
par └─┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
st └──────────────────────────────────────────────
530
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
531 /-- Insert a list of key-value pairs into the map. (Modifies `m` in-place when applicable) -/
532 def insert_all (l : list (Σ a, β a)) (m : hash_map α β) : hash_map α β :=
id └──┘ ┴ ┴┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴
src └──┘ ┴ ┴ └──────┘ └──────┘
typ └──┘ ┴ ┴┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴
doc └──────┘ └──────┘
533 l.foldl (λ m ⟨a, b⟩, insert m a b) m
id ┴└────┘ ┴ ┴┴ ┴ └────┘ ┴ ┴
src └────┘ └────┘
typ ┴└────┘ ┴ ┴┴ ┴ └────┘ ┴ ┴
doc └────┘
534
535 /-- Construct a hash map from a list of key-value pairs. -/
536 def of_list (l : list (Σ a, β a)) (hash_fn) : hash_map α β :=
id └──┘ ┴ ┴┴ ┴ ┴ └──────┘ ┴ ┴
src └──┘ ┴ ┴ └──────┘
typ └──┘ ┴ ┴┴ ┴ ┴ └──────┘ ┴ ┴
doc └──────┘
537 insert_all l (mk_hash_map hash_fn (2 * l.length))
id └────────┘ ┴ └─────────┘ └─────┘ ┴ ┴└─────┘
src └────────┘ └─────────┘ ┴ └─────┘
typ └────────┘ ┴ └─────────┘ └─────┘ ┴ ┴└─────┘
doc └────────┘ └─────────┘
538
539 /-- Remove a key from the map. (Modifies `m` in-place when applicable) -/
540 def erase (m : hash_map α β) (a : α) : hash_map α β :=
id └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
src └──────┘ └──────┘
typ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
doc └──────┘ └──────┘
541 match m with ⟨hash_fn, size, n, buckets, v⟩ :=
id ┴ └─────┘ └──┘ ┴ └─────┘ ┴
typ ┴ └─────┘ └──┘ ┴ └─────┘ ┴
542 if hc : contains_aux a (buckets.read hash_fn a) then
id └┘ └──────────┘ ┴ └───┘ ┴
src └┘ └──────────┘ └───┘
typ └┘ └──────────┘ ┴ └───┘ ┴
doc └──────────┘ └───┘
543 { hash_fn := hash_fn,
544 size := size - 1,
id ┴
src ┴
typ ┴
545 nbuckets := n,
546 buckets := buckets.modify hash_fn a (erase_aux a),
id └─────┘ ┴ └───────┘ ┴
src └─────┘ └───────┘
typ └─────┘ ┴ └───────┘ ┴
doc └─────┘ └───────┘
547 is_valid := v.erase _ a hc }
id └────┘ ┴ └┘
src └────┘
typ └────┘ ┴ └┘
548 else m
id ┴
typ ┴
549 end
550
551 theorem mem_erase : Π (m : hash_map α β) (a a' b'),
id ┴ └──────┘ ┴ ┴ ┴ └┘ └┘
src └──────┘
typ ┴ └──────┘ ┴ ┴ ┴ └┘ └┘
doc └──────┘
552 (sigma.mk a' b' : sigma β) ∈ (m.erase a).entries ↔
id └──────┘ └┘ └┘ └───┘ ┴ ┴ ┴└────┘ ┴ └─────┘ ┴
src └──────┘ └───┘ ┴ └────┘ └─────┘ ┴
typ └──────┘ └┘ └┘ └───┘ ┴ ┴ ┴└────┘ ┴ └─────┘ ┴
doc └────┘ └─────┘
553 a ≠ a' ∧ sigma.mk a' b' ∈ m.entries
id ┴ ┴ └┘ ┴ └──────┘ └┘ └┘ ┴ ┴└──────┘
src ┴ ┴ └──────┘ ┴ └──────┘
typ ┴ ┴ └┘ ┴ └──────┘ └┘ └┘ ┴ ┴└──────┘
doc └──────┘
554 | ⟨hash_fn, size, n, bkts, v⟩ a a' b' := begin
st └─────
555 let bkt := bkts.read hash_fn a,
id └───────┘ └─────┘ ┴
src └─────────┘└───────┘┴ ┴
typ └─────────┘└───────┘┴└─────┘┴┴
doc └─────────┘└───────┘┴ ┴
txt └─────────┘ ┴ ┴
par └─────────┘ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴
st ───────────────────────────────┘└─
556 by_cases Hc : (contains_aux a bkt : Prop),
id └──────────┘ ┴ └─┘
src └───────┘ └─┘ └──────────┘┴ ┴ └─┘ ┴
typ └───────┘ └─┘ └──────────┘┴┴┴└─┘└─┘ ┴
doc └───────┘ └─┘ └──────────┘┴ ┴ └─┘ ┴
txt └───────┘ └─┘ ┴ ┴ └─┘ ┴
par └───────┘ └─┘ ┴ ┴ └─┘ ┴
pid ┴ └─┘ ┴ ┴ └─┘ ┴
st ──────────────────────────────────────────┘└─
557 { let bkts' := bkts.modify hash_fn a (erase_aux a),
id └─────────┘ └─────┘ └───────┘ ┴
src └───────────┘└─────────┘┴ ┴ ┴ └───────┘┴ ┴
typ └───────────┘└─────────┘┴└─────┘┴ ┴ └───────┘┴┴┴
doc └───────────┘└─────────┘┴ ┴ ┴ └───────┘┴ ┴
txt └───────────┘ ┴ ┴ ┴ ┴ ┴
par └───────────┘ ┴ ┴ ┴ ┴ ┴
pid └───────┘┴└─┘ ┴ ┴ ┴ ┴ ┴
st ───┘└──────────────────────────────────────────────┘└─
558 suffices : sigma.mk a' b' ∈ bkts'.as_list ↔ a ≠ a' ∧ sigma.mk a' b' ∈ bkts.as_list,
id ┴ └───────────┘ ┴ ┴ └──────┘ └┘ └┘ └──────────┘
src └─────────┘ ┴ ┴ ┴┴┴└───────────┘┴ ┴ ┴┴┴ ┴ ┴└──────┘┴ ┴ ┴ ┴└──────────┘
typ └─────────┘ ┴ ┴ ┴┴┴└───────────┘┴ ┴┴┴┴┴ ┴ ┴└──────┘┴└┘┴└┘┴ ┴└──────────┘
doc └─────────┘ ┴ ┴ ┴ ┴└───────────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──────────┘
txt └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───────┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────────────────┘└─
559 { simpa [erase, @dif_pos (contains_aux a bkt) _ Hc] },
id └───┘ └─────┘ └──────────┘ ┴ └─┘ └┘
src └─────┘└───┘└┘ └─────┘┴ └──────────┘┴ ┴ └──┘ └┘
typ └─────┘└───┘└┘ └─────┘┴ └──────────┘┴┴┴└─┘└──┘└┘└┘
doc └─────┘└───┘└┘ ┴ └──────────┘┴ ┴ └──┘ └┘
txt └─────┘ └┘ ┴ ┴ ┴ └──┘ └┘
par └─────┘ └┘ ┴ ┴ ┴ └──┘ └┘
pid ┴┴ └┘ ┴ ┴ ┴ └──┘ ┴┴
st ─────┘└────────────────────────────────────────────────┘└┘└
560 have nd := v.nodup (mk_idx n (hash_fn a)),
id └─────┘ └────┘ ┴ └─────┘ ┴
src └─────────┘└─────┘┴ └────┘┴ ┴ ┴ └┘
typ └─────────┘└─────┘┴ └────┘┴┴┴ └─────┘┴┴└┘
doc └─────────┘ ┴ └────┘┴ ┴ ┴ └┘
txt └─────────┘ ┴ ┴ ┴ ┴ └┘
par └─────────┘ ┴ ┴ ┴ ┴ └┘
pid └─────┘┴└─┘ ┴ ┴ ┴ ┴ └┘
st ────────────────────────────────────────────┘└─
561 rcases valid.erase_aux a bkt ((contains_aux_iff nd).1 Hc) with ⟨u', w', b, hl', hfl'⟩,
id └─────────────┘ ┴ └─┘ └──────────────┘ └┘ └┘
src └─────┘└─────────────┘┴ ┴ ┴ └──────────────┘┴ └──┘ └───────────────────────────┘
typ └─────┘└─────────────┘┴┴┴└─┘┴ └──────────────┘┴└┘└──┘└┘└───────────────────────────┘
doc └─────┘ ┴ ┴ ┴ ┴ └──┘ └───────────────────────────┘
txt └─────┘ ┴ ┴ ┴ ┴ └──┘ └───────────────────────────┘
par └─────┘ ┴ ┴ ┴ ┴ └──┘ └───────────────────────────┘
pid ┴ ┴ ┴ ┴ ┴ └──┘ └───────────────────────────┘
st ────────────────────────────────────────────────────────────────────────────────────────┘└─
562 rcases append_of_modify u' [⟨a, b⟩] [] _ hl' hfl' with ⟨u, w, hl, hfl⟩,
id └──────────────┘ └┘ ┴ ┴ ┴ ┴ └┘ └─┘ └──┘
src └─────┘└──────────────┘┴ ┴┴ └┘ ┴┴┴└┘└─┘ ┴ └───────────────────┘
typ └─────┘└──────────────┘┴└┘┴┴ ┴└┘┴┴┴┴└┘└─┘└─┘┴└──┘└───────────────────┘
doc └─────┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ └───────────────────┘
txt └─────┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ └───────────────────┘
par └─────┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ └───────────────────┘
pid ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ └───────────────────┘
st ─────────────────────────────────────────────────────────────────────────┘└─
563 suffices : ∀_:sigma.mk a' b' ∈ u ∨ sigma.mk a' b' ∈ w, a ≠ a',
id ┴ ┴ └──────┘ └┘ ┴ ┴ └┘
src └─────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴└──────┘┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────────┘ └┘ ┴ ┴ ┴ ┴┴┴┴┴└──────┘┴ ┴└┘┴ ┴┴ ┴┴┴ ┴└┘
doc └─────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───────┘└┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────┘└─
564 { have : sigma.mk a' b' ∈ u ∨ sigma.mk a' b' ∈ w ↔ (¬a = a' ∧ a' = a) ∧ b' == b ∨
id ┴ └┘ ┴
src └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴└┘┴ ┴ └
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴└┘┴┴┴ └
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └
st ─────┘└───────────────────────────────────────────────────────────────────────────────
565 ¬a = a' ∧ (sigma.mk a' b' ∈ u ∨ sigma.mk a' b' ∈ w),
id ┴ ┴ └──────┘ └┘ └┘ ┴
src ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──────┘┴ ┴ ┴ ┴ ┴
typ ───────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴└──────┘┴└┘┴└┘┴ ┴┴┴
doc ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────┘└─
566 { simp [eq_comm, not_and_self_iff, and_iff_right_of_imp this] },
id └─────┘ └──────────────┘ └──────────────────┘ └──┘
src └────┘└─────┘└┘└──────────────┘└┘└──────────────────┘┴ └┘
typ └────┘└─────┘└┘└──────────────┘└┘└──────────────────┘┴└──┘└┘
doc └────┘ └┘ └┘ ┴ └┘
txt └────┘ └┘ └┘ ┴ └┘
par └────┘ └┘ └┘ ┴ └┘
pid ┴┴ └┘ └┘ ┴ ┴┴
st ───────┘└──────────────────────────────────────────────────────────┘└┘└
567 simpa [hl, show bkts'.as_list = _, from hfl, and_or_distrib_left,
id └┘ └───────────┘ ┴ └─┘ └─────────────────┘
src └─────┘ └┘ ┴└───────────┘┴ └───────┘ └┘└─────────────────┘└─
typ └─────┘└┘└┘ ┴└───────────┘┴┴└───────┘└─┘└┘└─────────────────┘└─
doc └─────┘ └┘ ┴└───────────┘┴ └───────┘ └┘ └─
txt └─────┘ └┘ ┴ ┴ └───────┘ └┘ └─
par └─────┘ └┘ ┴ ┴ └───────┘ └┘ └─
pid ┴┴ └┘ ┴ ┴ └───────┘ └┘ └─
st ────────────────────────────────────────────────────────────────────────
568 and_comm, and.left_comm, or.left_comm] },
id └──────┘ └───────────┘ └──────────┘
src ────────────┘└──────┘└┘└───────────┘└┘└──────────┘└┘
typ ────────────┘└──────┘└┘└───────────┘└┘└──────────┘└┘
doc ────────────┘ └┘ └┘ └┘
txt ────────────┘ └┘ └┘ └┘
par ────────────┘ └┘ └┘ └┘
pid ────────────┘ └┘ └┘ ┴┴
st ───────────────────────────────────────────────────┘└┘└
569 intros m e, subst a', revert m, apply not_or_distrib.2,
id └┘ └────────────┘
src └────────┘ └────┘ └──────┘ └────┘└────────────┘└┘
typ └────────┘ └────┘└┘ └──────┘ └────┘└────────────┘└┘
doc └────────┘ └────┘ └──────┘ └────┘ └┘
txt └────────┘ └────┘ └──────┘ └────┘ └┘
par └────────┘ └────┘ └──────┘ └────┘ └┘
pid └──┘ ┴ └┘ ┴ └┘
st ─────────────┘└────────┘└────────┘└──────────────────────┘└─
570 have nd' := v.as_list_nodup _,
id └─────────────┘
src └──────────┘└─────────────┘└┘
typ └──────────┘└─────────────┘└┘
doc └──────────┘ └┘
txt └──────────┘ └┘
par └──────────┘ └┘
pid └──────┘┴└─┘ └┘
st ────────────────────────────────┘└─
571 simp [hl, list.nodup_append] at nd', simp [nd'] },
id └┘ └───────────────┘ └─┘
src └────┘ └┘└───────────────┘└──────┘ └────┘ └┘
typ └────┘└┘└┘└───────────────┘└──────┘ └────┘└─┘└┘
doc └────┘ └┘ └──────┘ └────┘ └┘
txt └────┘ └┘ └──────┘ └────┘ └┘
par └────┘ └┘ └──────┘ └────┘ └┘
pid ┴┴ └┘ ┴┴└────┘ ┴┴ ┴┴
st ──────────────────────────────────────┘└───────────┘└┘└
572 { suffices : ∀_:sigma.mk a' b' ∈ bucket_array.as_list bkts, a ≠ a',
id └┘ └──┘ ┴ └┘
src ┴
typ ┴ └┘ └──┘ ┴ └┘
doc ┴
txt ┴
par ┴
pid ┴
st ────┘
573 { simp [erase, @dif_neg (contains_aux a bkt) _ Hc, entries, and_iff_right_of_imp this] },
id ┴
typ ┴
st └┘
574 intros m e, subst a',
id └┘
typ └┘
575 exact Hc ((v.contains_aux_iff _ _).2 (list.mem_map_of_mem sigma.fst m)) }
st └─
576 end
st ──┘
577
578 theorem find_erase_eq (m : hash_map α β) (a : α) : (m.erase a).find a = none :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
579 begin
580 cases h : (m.erase a).find a with b, {refl},
st └┘
581 exact absurd rfl ((mem_erase m a a b).1 ((find_iff (m.erase a) a b).1 h)).left
id ┴ ┴
typ ┴ ┴
582 end
st └─┘
583
584 theorem find_erase_ne (m : hash_map α β) (a a' : α) (h : a ≠ a') :
id ┴ ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ └┘
585 (m.erase a).find a' = m.find a' :=
id ┴ └┘ └┘
typ ┴ └┘ └┘
586 option.eq_of_eq_some $ λb',
id └┘
typ └┘
587 (find_iff _ _ _).trans $ (mem_erase m a a' b').trans $
id ┴ └┘ └┘
typ ┴ └┘ └┘
588 (and_iff_right h).trans (find_iff _ _ _).symm
id ┴
typ ┴
589
590 theorem find_erase (m : hash_map α β) (a' a : α) :
id ┴ ┴ ┴
typ ┴ ┴ ┴
591 (m.erase a).find a' = if a = a' then none else m.find a' :=
id ┴ └┘ ┴ └┘ └┘
typ ┴ └┘ ┴ └┘ └┘
592 if h : a = a' then by subst a'; simp [find_erase_eq m a]
id ┴ └┘ ┴
typ ┴ └┘ ┴
593 else by rw if_neg h; exact find_erase_ne m a a' h
id ┴ ┴ └┘ ┴
typ ┴ ┴ └┘ ┴
594
595 section string
596 variables [has_to_string α] [∀ a, has_to_string (β a)]
id └──┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └──┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
597 open prod
598 private def key_data_to_string (a : α) (b : β a) (first : bool) : string :=
id ┴ ┴ ┴ └──┘ └────┘
src └──┘ └────┘
typ ┴ ┴ ┴ └──┘ └────┘
599 (if first then "" else ", ") ++ sformat!"{a} ← {b}"
id └┘ └┘
typ └┘ └┘
600
601 private def to_string (m : hash_map α β) : string :=
id ┴ ┴ └────┘
src └────┘
typ ┴ ┴ └────┘
602 "⟨" ++ (fst (fold m ("", tt) (λ p a b, (fst p ++ key_data_to_string a b (snd p), ff)))) ++ "⟩"
id └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
src └┘ └┘
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
603
604 instance : has_to_string (hash_map α β) :=
id ┴ ┴
typ ┴ ┴
605 ⟨to_string⟩
606
607 end string
608
609 section format
610 open format prod
611 variables [has_to_format α] [∀ a, has_to_format (β a)]
id ┴ └──┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └──┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
612
613 private meta def format_key_data (a : α) (b : β a) (first : bool) : format :=
id ┴ ┴ ┴ └──┘ └──┘ ┴
src └──┘ └──┘ ┴
typ ┴ ┴ ┴ └──┘ └──┘ ┴
614 (if first then to_fmt "" else to_fmt "," ++ line) ++ to_fmt a ++ space ++ to_fmt "←" ++ space ++ to_fmt b
id └───┘ └──┘ ┴ └───┘ └───┘ ┴
src └──┘ └───┘ └───┘
typ └───┘ └──┘ ┴ └───┘ └───┘ ┴
615
616 private meta def to_format (m : hash_map α β) : format :=
id ┴ ┴ └────┘
src └────┘
typ ┴ ┴ └────┘
617 group $ to_fmt "⟨" ++ nest 1 (fst (fold m (to_fmt "", tt) (λ p a b, (fst p ++ format_key_data a b (snd p), ff)))) ++
id ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘
src ┴ └┘ └┘ └┘
typ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘
618 to_fmt "⟩"
619
620 meta instance : has_to_format (hash_map α β) :=
id ┴ ┴
typ ┴ ┴
621 ⟨to_format⟩
622 end format
623 end hash_map